- ∀p,I,L1,V. G ⊢ ⬈*[h, V] 𝐒⦃L1⦄ →
- ∀Y,T. G ⊢ ⬈*[h, T] 𝐒⦃Y⦄ →
- ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
+ ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒⦃L1⦄ →
+ ∀Y,T. G ⊢ ⬈*[h,T] 𝐒⦃Y⦄ →
+ ∀L2. Y = L2.ⓑ{I}V → ⦃G,L1⦄ ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*[h,ⓑ{p,I}V.T] 𝐒⦃L2⦄.