#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝 … f)
/3 width=6 by lifts_div3, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)
#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝 … f)
/3 width=6 by lifts_div3, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)