L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2.
#RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push1 … H) -H
#I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
qed-.
lemma sex_inv_tl: ∀RN,RP,f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2.
#RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push1 … H) -H
#I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
qed-.
lemma sex_inv_tl: ∀RN,RP,f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →