-lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx_ext h G) cfull.
-/2 width=7 by cpx_frees_conf_lexs/ qed-.
+lemma lfpx_fle_comp: ∀h,G. lfxs_fle_compatible (cpx h G).
+#h #G #L1 #L2 #T * #f1 #Hf1 #HL12
+elim (cpx_frees_conf_lexs h … Hf1 … HL12 T) // #f2 #Hf2
+lapply (lexs_fwd_length … HL12)
+/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *)
+qed-.