∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 &
U2 = ⓓ{a}V2.T2
) ∨
- â\88\83â\88\83T2. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[h, g] T2 & â\87§[0, 1] U2 ≡ T2 & a = true.
+ â\88\83â\88\83T2. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[h, g] T2 & â¬\86[0, 1] U2 ≡ T2 & a = true.
#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
#U0 #U2 #_ #HU02 * *
[ #V0 #T0 #HV10 #HT10 #H destruct