-axiom lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
+lemma lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
+#d #e #T #U1 #H elim H -H d e T U1
+[ #k #d #e #X #HX
+ lapply (lift_inv_sort1 … HX) -HX //
+| #i #d #e #Hid #X #HX
+ lapply (lift_inv_lref1_lt … HX ?) -HX //
+| #i #d #e #Hdi #X #HX
+ lapply (lift_inv_lref1_ge … HX ?) -HX //
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+ elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+ elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+]
+qed.