-lemma frees_lexs_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f →
- ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
-/2 width=7 by frees_tdeq_conf_lexs, tdeq_refl/ qed-.
-
-lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq_ext h o) cfull.
-/3 width=7 by frees_tdeq_conf_lexs, ex2_intro/ qed-.
+lemma frees_lfdeq_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f →
+ ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
+/2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ qed-.