#R #HR #L1 #L2 #T *
/5 width=7 by rexs_tc, sex_inv_tc_dx, sex_co, ext2_inv_tc, ext2_refl/
qed.
lemma rexs_lex_req: ∀R. c_reflexive … R →
∀L1,L. L1 ⪤[CTC … R] L → ∀L2,T. L ≡[T] L2 →
#R #HR #L1 #L2 #T *
/5 width=7 by rexs_tc, sex_inv_tc_dx, sex_co, ext2_inv_tc, ext2_refl/
qed.
lemma rexs_lex_req: ∀R. c_reflexive … R →
∀L1,L. L1 ⪤[CTC … R] L → ∀L2,T. L ≡[T] L2 →