-lemma rpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → ∀p.
- ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≛[T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V.
+lemma rpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G,L1.ⓑ{I}V1⦄ ⊢ ⬈[h,T] L2 → ∀p.
+ ∃∃L,V. ⦃G,L1⦄ ⊢ ⬈[h,ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≛[T] L2 & ⦃G,L1⦄ ⊢ V1 ⬈[h] V.