∀L2. L ⪤[RN,CTC … RP,f] L2 → L1⪤ [RN,CTC … RP,f] L2.
#RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L
[ #f #_ #Y #H -HRP >(sex_inv_atom1 … H) -Y // ]
∀L2. L ⪤[RN,CTC … RP,f] L2 → L1⪤ [RN,CTC … RP,f] L2.
#RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L
[ #f #_ #Y #H -HRP >(sex_inv_atom1 … H) -Y // ]