∀L1,L2,T. L1 ⪤[CTC … R] L2 → L1 ⪤*[R,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.
∀L1,L2,T. L1 ⪤[CTC … R] L2 → L1 ⪤*[R,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.