qed.
fact csx_appl_theta_aux (h) (G):
- â\88\80p,L,U. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â¬\86*[1] V1 ≘ V2 →
+ â\88\80p,L,U. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â\87§*[1] V1 ≘ V2 →
∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
#h #G #p #L #X #H
@(csx_ind_cpxs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
lemma csx_appl_theta (h) (G):
∀p,L,V,V2,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
- â\88\80V1. â¬\86*[1] V1 ≘ V2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+ â\88\80V1. â\87§*[1] V1 ≘ V2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
/2 width=5 by csx_appl_theta_aux/ qed.