∀V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ →
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄.
#h #o #p #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/
∀V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ →
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄.
#h #o #p #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/