+(* Advanced properties ******************************************************)
+
+lemma tc_lfxs_sym: ∀R. lfxs_fle_compatible R →
+ (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
+ ∀T. symmetric … (tc_lfxs R T).
+#R #H1R #H2R #T #L1 #L2 #H elim H -L2
+/4 width=3 by lfxs_sym, tc_lfxs_step_sn, inj/
+qed-.
+