-lemma rpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 →
- ∧∧ ⦃G, L1⦄ ⊢ ⬈[h, V] L2 & ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V.
+lemma rpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G,L1⦄ ⊢ ⬈[h,ⓑ{p,I}V.T] L2 →
+ ∧∧ ⦃G,L1⦄ ⊢ ⬈[h,V] L2 & ⦃G,L1.ⓑ{I}V⦄ ⊢ ⬈[h,T] L2.ⓑ{I}V.