∀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/