Existence of solidity witness implies the existence of standard solidity witness My question comes from M. Zeman' and R. Schindler's fine structure article in the handbook of set theory, the proof of lemma $7.4$. I understand most of the proof, except for one crucial claim, which I don't see how to prove.
First let $M$ be acceptable and $\nu\in p\in P_M$ and let $(W, r)$ be a witness for $\nu\in p$ w.r.t. $M, p$ such that $W\in M$. We want to show that $W^{\nu,p}_M \in M$, i.e. $M$ has the standard witness.
Now we let $\sigma:W^{\nu,p}_M\rightarrow_1 M$ be the inverse of the collapsing function, and we construct some $\sigma^*:W^{\nu,p}_M \rightarrow_1 \bar{W}$, where $\bar{W} = J^A_\alpha$, $\alpha = \mbox{sup}(h_W(\nu\cup \{r\})\cap\mbox{On})$ and $W = J^A_\beta$ for some $\beta \ge \alpha$. Now the authors assume wlog that $W^{\nu,p}_M$ is not an initial segment of $M$. Then it is shown that $\nu$ must be the critical point of $\sigma$. Then it is mentioned that if $M = J^B_\gamma$, then we know that $\sigma(\nu)$ is regular in $M$ and that $J^B_{\sigma(\nu)}\models\mbox{ZFC}^-$. And that we may code $W^{\nu,p}_M$ by some $a\subseteq \nu$, $\Sigma_1$-definably over $W^{\nu,p}_M$. $(*)$ And using $\sigma^*$ we have $a\in M$, in fact $a\in J^B_{\sigma(\nu)}$ by acceptability. And now, we can decode $a$ in $J^B_{\sigma(\nu)}$ and so $W^{\nu,p}_M \in J^B_{\sigma(\nu)} \subseteq M$.
Now I have the following question:
My question is about $(*)$. I don't see how we can code all of $W^{\nu,p}_M$ in some $a \subseteq \nu$, without using the parameter $\sigma^{-1}(p\setminus\nu+1)$. And that's because we only have $W^{\nu,p}_M = h_{W^{\nu,p}_M}"(\nu\cup \{\sigma^{-1}(p\setminus\nu+1)\})$. But if we manage to show that $p\setminus\nu+1\in J^B_{\sigma(\nu)}$, then we can use $p\setminus\nu+1$ as a parameter to define $a$ and decode it in $J^B_{\sigma(\nu)}$. Can we show this? Or is there another way to code $a$?
I would appreciate any hints or remarks for my above question. Thanks.
 A: The set $a$ is taken to incorporate the relevant information about $\sigma^{-1}(p\backslash(\nu+1))$ (and parameters ${<\nu}$). But since $\sigma^{-1}(p\backslash(\nu+1))$
is finite, we don't actually need to literally refer to that object itself; it can be coded.
That is, what one wants, uncoded, is the $\Sigma_1$-theory in $M$ of parameters in $\nu\cup\{p\backslash(\nu+1)\})$. But let's modify this slightly, and instead let $t$ be the set of all pairs $(\varphi,\vec{x})$ such that $\varphi$ is a $\Sigma_1$ formula (in the appropriate language), $\vec{x}\in\nu^{<\omega}$ and $M\models\varphi(\vec{x},p\backslash(\nu+1))$. So $t\subseteq\omega\times\nu^{<\omega}$, but use a simply definable bijection to convert this to a subset $a\subseteq\nu$. This is the kind of set $a$ you want to use.
(Another standard way to proceed is to replace the set $\nu\cup\{p\backslash(\nu+1)\}$ with $\nu$, by replacing (the finitely many elements in) $p\backslash(\nu+1)$ with some integers $0,1,\ldots,k-1$, and shifting the original integers up by $k$ to avoid conflicts.)
