-lemma lpx_drop_trans_O1: ∀h,o,G. dropable_dx (lpx h o G).
-/2 width=3 by lpx_sn_dropable/ qed-.
+lemma lfpx_drops_conf: ∀h,G. dropable_sn (cpx h G).
+/2 width=5 by lfxs_dropable_sn/ qed-.
+
+lemma lfpx_drops_trans: ∀h,G. dropable_dx (cpx h G).
+/2 width=5 by lfxs_dropable_dx/ qed-.