The covering lemma for L[U] (minimal k-model) is stated in Mitchel's handbook chapter:
"Assuming zero-dagger does not exist then covering holds for L[U] or there is a sequence C ⊆ κ, which is Prikry generic over L[U], such that for all sets x of ordinals there is a set y ∈ L[U,C] such that y ⊇ x and |y| = |x| + ℵ1."
And so a Prikry sequence is the only counter example to covering. Kanamori (19.18) proves a theorem of Solovay saying that the critical points of an iteration define a Prikry sequence. So in the core model L[U] (under zero-dagger) we must have prikry sequences.
What are the main differences between the proof of the (more familiar) covering lemma for L and the theorem above for L[U]? I assume that since the mice of L[U] are not simple $L_\alpha$'s we get indiscernibles when trying to cover a set X in a collapsed model. But is the proof the same as before "modulu" Prikry sequences, or is it more complicated than that and more cases should be handled regarding these sequences?