-lemma lfxs_sym: ∀R. lexs_frees_confluent (cext2 R) cfull →
- (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
- ∀T. symmetric … (lfxs R T).
-#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1
-/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/
-qed-.
-