-lemma lift_iref_bi (t1) (t2) (n):
- t1 ⇔ t2 → 𝛗n.t1 ⇔ 𝛗n.t2.
-/2 width=1 by subset_equivalence_ext_f1_bi/
-qed.
-
-lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
- (𝛗f@⧣❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
-#f #t #n #p * #q * #r #Hr #H1 #H2 destruct
-@(ex2_intro … (𝗱n◗𝗺◗r))
+lemma lift_term_iref_pap_sn (f) (t:prototerm) (k:pnat):
+ (𝛕f@⧣❨k❩.↑[⇂*[k]f]t) ⊆ ↑[f](𝛕k.t).
+#f #t #k #p * #q * #r #Hr #H1 #H2 destruct
+@(ex2_intro … (𝗱k◗𝗺◗r))