+
+lemma lexs_sdj_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 →
+ ∀f,L1,L2. L1 ⪤*[R1, RP, f] L2 → ∀g. f ∥ g →
+ ∃∃L. L1 ⪤*[RP, R1, 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 #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
+[ elim (sdj_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
+ elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/
+| elim (sdj_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,I1,I2. Decidable (RN L I1 I2)) →
+ (∀L,I1,I2. Decidable (RP L I1 I2)) →
+ ∀L1,L2,f. Decidable (L1 ⪤*[RN, RP, f] L2).
+#RN #RP #HRN #HRP #L1 elim L1 -L1 [ * | #L1 #I1 #IH * ]
+[ /2 width=1 by lexs_atom, or_introl/
+| #L2 #I2 #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 #f elim (IH L2 (⫱f)) -IH #HL12
+ [2: /4 width=3 by lexs_fwd_bind, or_intror/ ]
+ elim (pn_split f) * #g #H destruct
+ [ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -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-.