-lemma unwind2_term_iref_sn (f) (t) (n:pnat):
- ▼[f∘𝐮❨n❩]t ⊆ ▼[f](𝛕n.t).
-#f #t #n #p * #q #Hq #H0 destruct
-@(ex2_intro … (𝗱n◗𝗺◗q))
+lemma unwind2_term_iref_sn (f) (t) (k:pnat):
+ ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
+#f #t #k #p * #q #Hq #H0 destruct
+@(ex2_intro … (𝗱k◗𝗺◗q))