#RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
/3 width=3 by sex_next, TC_strap, inj/
qed.
lemma sex_tc_next_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (CTC … RN) L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 →
#RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
/3 width=3 by sex_next, TC_strap, inj/
qed.
lemma sex_tc_next_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (CTC … RN) L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 →