+lemma lift_term_iref_nap (f) (t) (n):
+ (𝛕↑(f@§❨n❩).↑[⇂*[↑n]f]t) ⇔ ↑[f](𝛕↑n.t).
+#f #t #n
+>tr_pap_succ_nap //
+qed.
+
+lemma lift_term_iref_uni (t) (n) (k):
+ (𝛕(k+n).t) ⇔ ↑[𝐮❨n❩](𝛕k.t).
+#t #n #k
+@(subset_eq_trans … (lift_term_iref_pap …))
+<tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
+/3 width=1 by iref_eq_repl, lift_term_id/
+qed.