-lemma lift_term_iref (f) (t) (k:pnat):
- (𝛕f@⧣❨k❩.↑[⇂*[k]f]t) ⇔ ↑[f](𝛕k.t).
-/3 width=1 by conj, lift_term_iref_sn, lift_term_iref_dx/
+lemma lift_term_iref_pap (f) (t) (k:pnat):
+ (𝛕f@⧣❨k❩.🠡[⇂*[k]f]t) ⇔ 🠡[f](𝛕k.t).
+/3 width=1 by conj, lift_term_iref_pap_sn, lift_term_iref_pap_dx/
+qed.
+
+lemma lift_term_iref_nap (f) (t) (n):
+ (𝛕↑(f@§❨n❩).🠡[⇂*[↑n]f]t) ⇔ 🠡[f](𝛕↑n.t).
+#f #t #n
+>tr_pap_succ_nap //