-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].