#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
/4 width=5 by sex_tc_next_sn, sex_tc_refl, trans_TC/
qed.
theorem sex_tc_push: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (CTC … RP) L1 I1 I2 → ∀L2. TC … (sex RN RP f) L1 L2 →
#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
/4 width=5 by sex_tc_next_sn, sex_tc_refl, trans_TC/
qed.
theorem sex_tc_push: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (CTC … RP) L1 I1 I2 → ∀L2. TC … (sex RN RP f) L1 L2 →