/3 width=7 by frees_tdeq_conf_lexs, lexs_refl/ qed-.
lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq h o) cfull.
/3 width=7 by frees_tdeq_conf_lexs, lexs_refl/ qed-.
lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq h o) cfull.