∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
#h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
#h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/