-lemma rex_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- rex_fsge_compatible R1 →
- ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤[R1,T] L2 → ∀p.
- ∃∃L,V. L1 ⪤[R1,ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤[R2,T] L2 & R1 L1 V1 V.
+lemma rex_bind_dx_split (R1) (R2):
+ (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+ rex_fsge_compatible R1 →
+ ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤[R1,T] L2 → ∀p.
+ ∃∃L,V. L1 ⪤[R1,ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤[R2,T] L2 & R1 L1 V1 V.