Mitchell, Steel. FSIT. Lemma 2.8: Is $k$-solidity actually needed? Consider the following result (which is Lemma 2.8 in Mitchell and Steel's paper on Fine Structure and Iteration Trees):
Lemma 2.8 Let $\pi \colon \mathcal{H} \to \mathcal{M}$ be generalized $r \Sigma_{k}$
  elementary, where $\mathcal M$ is a ppm (not of type III) and $1
  \leq k < \omega$. Suppose that $\rho_{k}^{\mathcal{M}} \subseteq
  \mathcal{H}$ and $\pi \restriction \rho_{k}^{\mathcal{M}} =
  \operatorname{id}$. Suppose also that $\pi(r)$ is the $k$th standard parameter of
  $(\mathcal{M}, \pi(q))$ and that $\pi(r)$ is $k$-solid and
  $k$-universal over $(\mathcal{M}, \pi(q))$. Then


*

*$\rho_{k}^{\mathcal{H}} = \rho_{k}^{\mathcal{M}}$,

*$r$ is the $k$th standard parameter of $(\mathcal{H},q)$ and 

*$r$ is $k$-universal over $(\mathcal{H}, q)$.


The proofs of items $1.$ and $2.$ are included in this paper and in
both cases it seems that the $k$-solidity of $\pi(r)$ over
$(\mathcal{M}, \pi(q))$ isn't actually needed. Hence I decided to
prove item $3.$ to see how $k$-solidity comes into play. However, if
my argument is correct, it doesn't rely on $k$-solidity either.
Here is my proof of item $3.$:
Proof (of $3.$). Let $A \in \mathcal{H}$ be such that $A \subseteq
  \rho_{k}^{\mathcal{H}}$. Then $\pi(A) \cap \rho_{k}^{\mathcal{M}}
  \in \mathcal M$. By the $k$-universality of $\pi(r)$ over
  $(\mathcal{M}, \pi(q))$ there is hence some generalized Skolem term
  $\tau \in S_{\kappa}$ and some $\vec{\alpha} \in ^{< \omega}
  \rho_{k}^{\mathcal{M}}$ s.t.
  $$
    \pi(A) \cap \rho_{k}^{\mathcal{M}} =
    \tau^{\mathcal{M}}[\vec{\alpha}, \pi(r), \pi(q)] \cap \rho_{k}^{\mathcal{M}}.
  $$
  Let $B := \tau^{\mathcal{H}}[\vec{\alpha},r,q] \cap \rho_{k}^{\mathcal{H}}$. Combining the fact
  that $\pi$ is generalized $r \Sigma_{k}$-elementary, $\rho_{k}^{\mathcal{H}}=
  \rho_{k}^{\mathcal{M}} \subseteq \mathcal{H}$ and $\pi \restriction
  \rho_{k}^{\mathcal M} = \operatorname{id}$ we have that
  \begin{align*}
    \mathcal{H} \models A \cap \rho_{k}^{\mathcal{H}} = B &\iff \mathcal{H} \models A \cap \rho_{k}^{\mathcal{H}} = \tau^{\mathcal
                                                            H}[\vec{\alpha},
                                                           r,q] \cap
                                                           \rho_{k}^{\mathcal{H}}
    \\
                                                        &\iff
                                                          \mathcal{M}
                                                          \models
                                                          \pi(A) \cap
                                                          \rho_{k}^{\mathcal{M}}
                                                          =
                                                          \tau^{\mathcal{M}}[\vec{\alpha},\pi(r),\pi(q)]
                                                          \cap \rho_{k}^{\mathcal{M}}.
  \end{align*}
  Since the last line is true, it follows that
  $A \cap \rho_{k}^{\mathcal{H}}
  =\tau^{\mathcal{H}}[\vec{\alpha},r,q] \cap \rho_{k}^{\mathcal{H}}$. Thus $r$ is indeed
  $k$-universal over $(\mathcal{H}, q)$. Q.E.D.
Question: Did I miss something and this result actually relies on the $k$-solidity of $\pi(r)$ over $(\mathcal{M},\pi(q))$ or can this assumption be dropped?
If $k$-solidity is needed, I'd like to understand where exactly in the proof it is used and ideally I'd like to see an example in which Lemma 2.8 fails without $k$-solidity.

PS: I am aware that this question isn't exactly 'ongoing research' and I strongly considered posting it over at MSE. However, since the group of people able to answer this question is more likely to be encountered here and since a somewhat similar question has been asked and well-received here, I decided to go with mathoverflow.
 A: In my question I already verified that (assuming 1. and 2.) item 3. is provable without assuming that $\pi(r)$ is $k$-solid over $(\mathcal{M},q)$. To see that we can actually drop $k$-solidity in this lemma, it hence suffices to see that 1. and 2. also don't require that $k$-solidity of $\pi(r)$.
If $\rho_{k}^{\mathcal{M}} = \operatorname{Ord}^{\mathcal{M}}$, then $\pi = \operatorname{id}$
  and the lemma trivially holds. Thus assume that
  $\rho_{k}^{\mathcal{M}} < \operatorname{Ord}^{\mathcal{M}}$.


*

*Let $\alpha \leq \rho_{k}^{\mathcal M}$. Since
$\pi \restriction \rho_{\kappa}^{\mathcal{M}} = \operatorname{id}$
and since $\pi$ is generalized $r \Sigma_{k}$-elementary, we have - up
to a slight abuse of notation -
\begin{align*}
  \operatorname{Th}_{k}^{\mathcal{H}}(\alpha \cup \{ s \})
  &= \{(\phi, \vec{a}, s) \mid \vec{a} \in ^{< \omega}{\alpha}
    \wedge \mathcal{H} \models \phi[\vec{a}, s] \} \\
  &= \{(\phi, \vec{a}, s) \mid \vec{a} \in ^{< \omega}{\alpha}
    \wedge \mathcal{M} \models \phi[\vec{a}, \pi(s)] \}
\end{align*}
In particular, for any $\phi \in r \Sigma_{k}$ and any $\vec{a} \in ^{<
  \omega}{\alpha}$, we have
$$
  (\phi, \vec{a}, s) \in
  \operatorname{Th}_{k}^{\mathcal{H}}(\alpha \cup \{s \}) \iff
  (\phi, \vec{a}, \pi(s)) \in
  \operatorname{Th}_{k}^{\mathcal{M}}(\alpha \cup \{ \pi(s) \}).
$$
By enlarging $\alpha$, if necessary, we may assume that $\alpha$
is primitive recursively closed and hence uniformly code
\begin{align*}
  \{(\phi, \vec{a}) \mid (\phi, \vec{a}, s) \in
  \operatorname{Th}_{k}^{\mathcal{H}}(\alpha \cup \{ s \}) \} \\
  = \{(\phi, \vec{a}) \mid (\phi, \vec{a}, \pi(s)) \in
  \operatorname{Th}_{k}^{\mathcal{M}}(\alpha \cup \{ \pi(s) \}) \}
\end{align*}
as a subset $A \subseteq \alpha$. Since
$\alpha < \rho_{k}^{\mathcal{M}}$, we have
$\operatorname{Th}_{k}^{\mathcal{M}}(\alpha \cup \{ \pi(s) \}) \in
\mathcal{M}$ and hence $A \in \mathcal{M}$. By the strong
acceptability of $\mathcal{M}$ - observing that
$\rho_{k}^{\mathcal{M}}$ is an $\mathcal{M}$-cardinal - this
yields
$$
  A \in \mathcal{J}_{\rho_{k}^{\mathcal{M}}}^{\mathcal M} = \left(
    H_{\rho_{k}^{\mathcal{M}}} \right)^{\mathcal{M}} \overset{\pi
    \restriction \rho_{k}^{\mathcal{M}} = \operatorname{id}}{=} \left(
    H_{\rho_{k}^{\mathcal{M}}}\right)^{\mathcal{H}} \subseteq \mathcal{H}.
$$
Therefore
$$
  \operatorname{Th}_{k}^{\mathcal{H}}(\alpha \cup \{ s \}) = \{
  (\phi, \vec{a}, s) \mid \langle \phi, \vec{a} \rangle \in A \}
  \in \mathcal{H}
$$
and $\rho_{k}^{\mathcal{M}} \leq \rho_{k}^{\mathcal{H}}$.
On the other hand, suppose that
$\rho_{k}^{\mathcal{M}} < \rho_{k}^{\mathcal{H}}$. Then
$\operatorname{Th}_{k}^{\mathcal{H}}(\rho_{k}^{\mathcal{M}} \cup
\{(r,q)\}) \in \mathcal{H}$. Let
$A \subseteq \rho_{k}^{\mathcal{M}}$, $A \in \mathcal{H}$ be a
uniform code for
$$
  \{ (\phi, \vec{a}) \mid (\phi, \vec{a}, (r,q)) \in
  \operatorname{Th}_{k}^{\mathcal{H}}(\rho_{k}^{\mathcal{M}} \cup
  \{(r,q)\})\}.
$$
Then $A = \pi(A) \cap \rho_{k}^{\mathcal{M}} \in \mathcal{M}$
witnesses (as above) that
$\operatorname{Th}_{k}^{\mathcal{M}}(\rho_{k}^{\mathcal{M}} \cup
\{ \pi(r), \pi(q)\}) \in \mathcal{M}$. This contradicts the fact
that $\pi(r)$ is the $k$th standard parameter of
$(\mathcal{M},\pi(q))$!

*The proof above also shows that
$\operatorname{Th}_{k}^{\mathcal{H}}(\rho_{k}^{\mathcal{H}} \cup
\{ (r,q)\}) \not \in \mathcal{H}$. Hence it suffices to show that
for all $s <_{\operatorname{lex}} r$
$$
  \operatorname{Th}_{k}^{\mathcal{H}}(\rho_{k}^{\mathcal{H}} \cup
  \{ (s,q)\}) \in \mathcal{H}.
$$
So, fix $s <_{\operatorname{lex}} r$. Then
$\pi(s)<_{\operatorname{lex}} \pi(r)$ and hence
$$
  \operatorname{Th}_{k}^{\mathcal{M}}(\rho_{k}^{\mathcal{H}} \cup
  \{ (\pi(s),\pi(q))\}) \in \mathcal{M}.
$$
Let $A \subseteq \rho_{k}^{\mathcal{M}}$, $A \in \mathcal{M}$ be
the code of this fact as above. Since $\pi(r)$ is $k$-universal
over $(M, \pi(q))$ there is some $\tau \in \operatorname{Sk}_{k}$
and $\vec{a} \in ^{< \omega}{\rho_{k}^{\mathcal{M}}}$ such that
$A = \tau^{\mathcal{M}}[\vec{a}, \pi(r), \pi(q)] \cap
\rho_{k}^{\mathcal{M}}$.  Let
$$
  B = \tau^{\mathcal{H}}[\vec{a}, \pi(r), \pi(q)] \cap
  \rho_{k}^{\mathcal{M}}.
$$
Since $\pi$ is generalized $r \Sigma_{k}$-elementary we have,
for all $\xi < \rho_{k}^{\mathcal{M}} = \rho_{k}^{\mathcal{H}}$
$$
  \mathcal{M} \models \xi \in
  \tau^{\mathcal{M}}[\vec{a},\pi(r),\pi(q)] \iff \mathcal{H}
  \models \xi \in \tau^{\mathcal{H}}[\vec{a},r,q].
$$
Thus $B = A \in \mathcal{H}$ witnesses that
$\operatorname{Th}_{k}^{\mathcal{H}}(\rho_{k}^{\mathcal{H}} \cup
\{(s,q)\}) \in \mathcal{H}$ and hence the
$<_{\operatorname{lex}}$-minimality of $r$.

