+
+lemma sex_sdj_split_dx (R1) (R2) (RP):
+ c_reflexive … R1 → c_reflexive … R2 → c_reflexive … RP →
+ ∀L1,f1.
+ (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
+ ∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
+ ∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
+#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1
+[ #f1 #_ #L2 #H #f2 #_
+ lapply (sex_inv_atom1 … H) -H #H destruct
+ /2 width=3 by sex_atom, ex2_intro/
+| #K1 #I1 #IH #f1 elim (pn_split f1) * #g1 #H destruct
+ #HR #L2 #H #f2 #Hf
+ [ elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
+ elim (sdj_inv_px … Hf ??) -Hf [1,3: * |*: // ] #g2 #Hg #H destruct
+ elim (IH … HK12 … Hg) -IH -HK12 -Hg
+ [1,3: /3 width=5 by sex_next, sex_push, ex2_intro/
+ |2,4: /3 width=3 by drops_drop/
+ ]
+ | elim (sex_inv_next1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
+ elim (sdj_inv_nx … Hf ??) -Hf [|*: // ] #g2 #Hg #H destruct
+ elim (IH … HK12 … Hg) -IH -HK12 -Hg
+ [ /5 width=11 by sex_next, sex_push, drops_refl, ex2_intro/
+ | /3 width=3 by drops_drop/
+ ]
+ ]
+]
+qed-.