-lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) →
- ∀L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 →
- ∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2.
-#RN #RP #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 //
-#I #L1 #L2 #V1 #V2 #f2 #_ #HV12 #IH
-[ * * [2: #n1 ] ] #f1 #H
-[ /4 width=5 by lexs_next, sle_inv_nn/
-| /4 width=5 by lexs_push, sle_inv_pn/
-| elim (sle_inv_xp … H) -H [2,3: // ]
+lemma lexs_sym: ∀RN,RP.
+ (∀L1,L2,I1,I2. RN L1 I1 I2 → RN L2 I2 I1) →
+ (∀L1,L2,I1,I2. RP L1 I1 I2 → RP L2 I2 I1) →
+ ∀f. symmetric … (lexs RN RP f).
+#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f
+/3 width=2 by lexs_next, lexs_push/
+qed-.
+
+lemma lexs_pair_repl: ∀RN,RP,f,I1,I2,L1,L2.
+ L1.ⓘ{I1} ⪤*[RN, RP, f] L2.ⓘ{I2} →
+ ∀J1,J2. RN L1 J1 J2 → RP L1 J1 J2 →
+ L1.ⓘ{J1} ⪤*[RN, RP, f] L2.ⓘ{J2}.
+/3 width=3 by lexs_inv_tl, lexs_fwd_bind/ qed-.
+
+lemma lexs_co: ∀RN1,RP1,RN2,RP2. RN1 ⊆ RN2 → RP1 ⊆ RP2 →
+ ∀f,L1,L2. L1 ⪤*[RN1, RP1, f] L2 → L1 ⪤*[RN2, RP2, f] L2.
+#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
+/3 width=1 by lexs_atom, lexs_next, lexs_push/
+qed-.
+
+lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 →
+ ∀f,L1,L2. L1 ⪤*[RN1, RP1, f] L2 → 𝐈⦃f⦄ →
+ L1 ⪤*[RN2, RP2, f] L2.
+#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
+#f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H
+[ elim (isid_inv_next … H) -H //
+| /4 width=3 by lexs_push, isid_inv_push/
+]
+qed-.
+
+lemma lexs_sdj: ∀RN,RP. RP ⊆ RN →
+ ∀f1,L1,L2. L1 ⪤*[RN, RP, f1] L2 →
+ ∀f2. f1 ∥ f2 → L1 ⪤*[RP, RN, f2] L2.
+#RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
+#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
+[ elim (sdj_inv_nx … H12) -H12 [2,3: // ]
+ #g2 #H #H2 destruct /3 width=1 by lexs_push/
+| elim (sdj_inv_px … H12) -H12 [2,4: // ] *
+ #g2 #H #H2 destruct /3 width=1 by lexs_next, lexs_push/
+]
+qed-.
+
+lemma sle_lexs_trans: ∀RN,RP. RN ⊆ RP →
+ ∀f2,L1,L2. L1 ⪤*[RN, RP, f2] L2 →
+ ∀f1. f1 ⊆ f2 → L1 ⪤*[RN, RP, f1] L2.
+#RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
+#f2 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f1 #H12
+[ elim (pn_split f1) * ]
+[ /4 width=5 by lexs_push, sle_inv_pn/
+| /4 width=5 by lexs_next, sle_inv_nn/
+| elim (sle_inv_xp … H12) -H12 [2,3: // ]