Let $E$ be a $(\kappa, \lambda)$-extender such that $j: V\to M\simeq Ult(V,E)$ is the corresponding elementary embedding with critical point $\kappa$, $M\supset V_{\kappa+2}$, $M^\kappa\subset M$. Let $\bar{U}$ be a sequence of ultrafilters over $V_\kappa$ of length greater than $\alpha$ where $0<\alpha<(2^\kappa)^+$. Let $E'= E|_{[\alpha]^{<\omega}}$ and $M'\simeq Ult(V,E')$. Notice that $V_{\kappa+2}^\alpha \subset M$ since any transitive closure of such sequence could be coded by a subset of $2^\kappa$ which lies in $V_{\kappa+2}$ so the original set could be recovered by taking transitive collapse in $M$. So $\bar{U}|\alpha \in M$.

My question is:

Is $\bar{U}|\gamma \in M'$ for all $\gamma<\alpha$? I believe it is not true, since if $\alpha=\kappa+1$, then the ultrapower by $E'$ is more or less ultrapower by $U(0)$, by $U(0)\not \in Ult(V,U(0))$ as we know.

The motivation is from a theorem that appeared in the chapter Prikry-type forcings in the Hankbook of Set theory, Lemma 5.1. Where the above is used in the proof to produce a measure sequence of length $\geq ({2^{\kappa} })^+$ from a $\kappa+2$-strong cardinal.

The way I convinced myself is as follows (with GCH): Let $E$ be a $(\kappa, \kappa^{++})$-extender such that $j: V\to M\simeq Ult(V,E)$ is the corresponding elementary embedding with critical point $\kappa$, $M\supset V_{\kappa+2}$, $M^\kappa\subset M$. Just as above $\bar{U}|\alpha \in M$ so there exists $\beta \in [\kappa^{++}]^{<\omega}, f: [\kappa^{++}]^{<\omega}\to V$ such that $j(f)(\beta)=\bar{U}|\alpha$, let $E'= E|_{[\alpha+\sup \beta +1]^{<\omega}}$ then $M'\simeq Ult(V,E')$ will contain $\bar{U}|\alpha$. Since $k: M'\to M$ defined by $k([f]_{U_\gamma})=j(f)(\gamma)$, which ensures that $\bar{U}|\alpha\in ran(k)$. But my concerns are: 1) GCH 2) The length of the restriction of the original extender is very likely to be longer than $\alpha$.

Maybe I'm just missing something basic so any pointer would be appreciated.