(* Basic_2A1: includes: lift_inj *)
lemma lifts_inj: ∀f. is_inj2 … (lifts f).
-#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx ð\9d\90\88ð\9d\90\9d … f)
+#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx ð\9d\90¢ … f)
/3 width=6 by lifts_div3, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)
lemma lifts_mono: ∀f,T. is_mono … (lifts f T).
-#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn ð\9d\90\88ð\9d\90\9d … f)
+#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn ð\9d\90¢ … f)
/3 width=6 by lifts_conf, lifts_fwd_isid/
qed-.