#RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L
[ #f #_ #Y #H -HRP >(sex_inv_atom1 … H) -Y // ]
#f #I1 #I #L1 #L #HL1 #HI1 #IH #Hf #Y #H
#RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L
[ #f #_ #Y #H -HRP >(sex_inv_atom1 … H) -Y // ]
#f #I1 #I #L1 #L #HL1 #HI1 #IH #Hf #Y #H