lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
/2 width=3 by csx_appl_beta_aux/ qed.
-fact csx_appl_theta_aux: â\88\80h,g,a,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, g] U â\86\92 â\88\80V1,V2. â\87§[0, 1] V1 ≡ V2 →
+fact csx_appl_theta_aux: â\88\80h,g,a,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, g] U â\86\92 â\88\80V1,V2. â¬\86[0, 1] V1 ≡ V2 →
∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
lapply (csx_fwd_pair_sn … HVT) #HV
]
qed-.
-lemma csx_appl_theta: â\88\80h,g,a,V1,V2. â\87§[0, 1] V1 ≡ V2 →
+lemma csx_appl_theta: â\88\80h,g,a,V1,V2. â¬\86[0, 1] V1 ≡ V2 →
∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
/2 width=5 by csx_appl_theta_aux/ qed.