| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
]
-qed.
+qed-.
(* Basic_1: was: lift_gen_lift *)
theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
| #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.
+qed-.
(* Basic_1: was: lift_free (left to right) *)
theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →