-lemma rpx_bind_repl_dx: ∀h,I,I1,G,L1,L2,T.
- ⦃G,L1.ⓘ{I}⦄ ⊢ ⬈[h,T] L2.ⓘ{I1} →
- ∀I2. ⦃G,L1⦄ ⊢ I ⬈[h] I2 →
- ⦃G,L1.ⓘ{I}⦄ ⊢ ⬈[h,T] L2.ⓘ{I2}.
+lemma rpx_bind_repl_dx (G):
+ ∀I,I1,L1,L2,T. ❪G,L1.ⓘ[I]❫ ⊢ ⬈[T] L2.ⓘ[I1] →
+ ∀I2. ❪G,L1❫ ⊢ I ⬈ I2 → ❪G,L1.ⓘ[I]❫ ⊢ ⬈[T] L2.ⓘ[I2].