-(* Basic_2A1: includes: lift_mono *)
-theorem lifts_mono: ∀t,T,U1. ⬆*[t] T ≡ U1 → ∀U2. ⬆*[t] T ≡ U2 → U1 = U2.
-#t #T #U1 #H elim H -t -T -U1
-[ /2 width=2 by lifts_inv_sort1/
-| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref1 … HX) -HX
- /4 width=4 by at_mono, eq_f/
-| /2 width=2 by lifts_inv_gref1/
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind1 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat1 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
-]
-qed-.
-