#R #HR #L1 #L2 #T *
/5 width=7 by tc_lfxs_tc, lexs_inv_tc_dx, lexs_co, ext2_inv_tc, ext2_refl/
qed.
lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R →
#R #HR #L1 #L2 #T *
/5 width=7 by tc_lfxs_tc, lexs_inv_tc_dx, lexs_co, ext2_inv_tc, ext2_refl/
qed.
lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R →