-lemma lreq_dedropable: dedropable_sn lreq.
-@lexs_liftable_dedropable
-/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl/
-qed-.
+lemma lreq_co_dedropable_sn: co_dedropable_sn lreq.
+@lexs_liftable_co_dedropable_sn
+/2 width=6 by cfull_lift_sn, ceq_lift_sn/ qed-.
+
+lemma lreq_co_dropable_sn: co_dropable_sn lreq.
+@lexs_co_dropable_sn qed-.