-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 (G):
+ ∀I,L1,L2,V1,T. ❪G,L1.ⓑ[I]V1❫ ⊢ ⬈[T] L2 → ∀p.
+ ∃∃L,V. ❪G,L1❫ ⊢ ⬈[ⓑ[p,I]V1.T] L & L.ⓑ[I]V ≛[T] L2 & ❪G,L1❫ ⊢ V1 ⬈ V.