-lemma cpxs_lifts: ∀h,G. d_liftable2 (cpxs h G).
-/3 width=10 by cpx_lifts, cpxs_strap1, d2_liftable_LTC/ qed-.
+lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpxs h G).
+/3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_CTC/ qed-.
+
+lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpxs h G).
+/3 width=12 by cpxs_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.