TC … (sex RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
/3 width=3 by sex_next, TC_strap, inj/
TC … (sex RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
/3 width=3 by sex_next, TC_strap, inj/