/3 width=1 by lexs_atom, lexs_next, lexs_push/
qed-.
+lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2.
+ (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) →
+ ∀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 #I #K1 #K2 #V1 #V2 #_ #HV12 #IH #H
+[ elim (isid_inv_next … H) -H //
+| /4 width=3 by lexs_push, isid_inv_push/
+]
+qed-.
+
lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) →
∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 →
∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2.
#g2 #H #H2 destruct /3 width=5 by lexs_next/
]
qed-.
+
+lemma lexs_sle_split: ∀R1,R2,RP. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+ ∀f,L1,L2. L1 ⦻*[R1, RP, f] L2 → ∀g. f ⊆ g →
+ ∃∃L. L1 ⦻*[R1, RP, g] L & L ⦻*[R2, cfull, f] L2.
+#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
+[ /2 width=3 by lexs_atom, ex2_intro/ ]
+#f #I #L1 #L2 #V1 #V2 #_ #HV12 #IH #y #H
+[ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
+ elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, ex2_intro/
+| elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
+ elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/
+]
+qed-.
+
+lemma lexs_dec: ∀RN,RP.
+ (∀L,T1,T2. Decidable (RN L T1 T2)) →
+ (∀L,T1,T2. Decidable (RP L T1 T2)) →
+ ∀L1,L2,f. Decidable (L1 ⦻*[RN, RP, f] L2).
+#RN #RP #HRN #HRP #L1 elim L1 -L1 [ * | #L1 #I1 #V1 #IH * ]
+[ /2 width=1 by lexs_atom, or_introl/
+| #L2 #I2 #V2 #f @or_intror #H
+ lapply (lexs_inv_atom1 … H) -H #H destruct
+| #f @or_intror #H
+ lapply (lexs_inv_atom2 … H) -H #H destruct
+| #L2 #I2 #V2 #f elim (eq_bind2_dec I1 I2) #H destruct
+ [2: @or_intror #H elim (lexs_fwd_pair … H) -H /2 width=1 by/ ]
+ elim (IH L2 (⫱f)) -IH #HL12
+ [2: @or_intror #H elim (lexs_fwd_pair … H) -H /2 width=1 by/ ]
+ elim (pn_split f) * #g #H destruct
+ [ elim (HRP L1 V1 V2) | elim (HRN L1 V1 V2) ] -HRP -HRN #HV12
+ [1,3: /3 width=1 by lexs_push, lexs_next, or_introl/ ]
+ @or_intror #H
+ [ elim (lexs_inv_push … H) | elim (lexs_inv_next … H) ] -H
+ /2 width=1 by/
+]
+qed-.