Дмитро, can you expand a bit on how you prove that every ℵ<sub>α+ω</sub> is measurable in the HOD of L[Card] and why the sequence of the ℵ<sub>α+n</sub>s is Prikry generic, assuming there is a sharp for an inner model with a proper class of measurable cardinals? Thanks, Ralf.