/3 width=6 by lifts_div, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)
lemma lifts_mono: ∀T,U1,f. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
/3 width=6 by lifts_div, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)
lemma lifts_mono: ∀T,U1,f. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.