- ∀T2. T1 ≡[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f.
-/4 width=7 by frees_tdeq_conf_lexs, lexs_refl, ext2_refl/ qed-.
-
-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-.
+ ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f.
+/4 width=7 by frees_tdeq_conf_lfdeq, lexs_refl, ext2_refl/ qed-.