∀V1,T1,U2. ⦃G,L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 →
∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G,L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 &
U2 = ⓓ{p}V2.T2
- | â\88\83â\88\83T2. â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88*[h] T2 & â¬\86*[1] U2 ≘ T2 & p = Ⓣ.
+ | â\88\83â\88\83T2. â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88*[h] T2 & â\87§*[1] U2 ≘ T2 & p = Ⓣ.
#h #p #G #L #V1 #T1 #U2 #H
@(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
#U0 #U2 #_ #HU02 * *