-lemma lift_inv_pair_xy_x: ∀l,m,I,V,T. ⬆[l, m] ②{I} V. T ≡ V → ⊥.
+lemma lift_inv_Y1: ∀T1,T2,m. ⬆[∞, m] T1 ≡ T2 → T1 = T2.
+#T1 elim T1 -T1 *
+[ #k #X #m #H lapply (lift_inv_sort1 … H) -H //
+| #i #X #m #H lapply (lift_inv_lref1_lt … H ?) -H //
+| #p #X #m #H lapply (lift_inv_gref1 … H) -H //
+| #a #I #V1 #T1 #IHV1 #IHT1 #X #m #H elim (lift_inv_bind1 … H) -H
+ #V2 #T2 #HV12 #HT12 #H destruct /3 width=2 by eq_f2/
+| #I #V1 #T1 #IHV1 #IHT1 #X #m #H elim (lift_inv_flat1 … H) -H
+ #V2 #T2 #HV12 #HT12 #H destruct /3 width=2 by eq_f2/
+]
+qed-.
+
+lemma lift_inv_pair_xy_x: ∀l,m,I,V,T. ⬆[l, m] ②{I}V.T ≡ V → ⊥.