- ∀p,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
- ∀b,f,L0,V0,W0,T0. ⬇*[b, f] L0 ≘ L → ⬆*[f] W ≘ W0 → ⬆*[⫯f] T ≘ T0 →
- ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
+ ∀p,G,L,W,T,A,B. ⦃G,L,W⦄ ϵ[RP] 〚B〛 → (
+ ∀b,f,L0,V0,W0,T0. ⬇*[b,f] L0 ≘ L → ⬆*[f] W ≘ W0 → ⬆*[⫯f] T ≘ T0 →
+ ⦃G,L0,V0⦄ ϵ[RP] 〚B〛 → ⦃G,L0,W0⦄ ϵ[RP] 〚B〛 → ⦃G,L0.ⓓⓝW0.V0,T0⦄ ϵ[RP] 〚A〛