- ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒⦃L1⦄ →
- ∀Y,T. G ⊢ ⬈*[h,T] 𝐒⦃Y⦄ →
- â\88\80L2. Y = L2.â\93§ â\86\92 â¦\83G,L1â¦\84 ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h,ⓑ{p,I}V.T] 𝐒⦃L2⦄.
+ ∀p,I,L1,V. G ⊢ ⬈*𝐒[h,V] L1 →
+ ∀Y,T. G ⊢ ⬈*𝐒[h,T] Y →
+ â\88\80L2. Y = L2.â\93§ â\86\92 â\9dªG,L1â\9d« ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L2.