update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_lfpx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma
index 2067df1b301081c9450f9d794fbd00e4112c36dd..44fc48fae862e8f787ed34ee71c31877b231f00c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma
@@ -60,7 +60,7 @@ elim (cpx_inv_abbr1 … H1) -H1 *
 ]
 qed.
 
-fact csx_appl_theta_aux: â\88\80h,o,p,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â¬\86*[1] V1 â\89¡ V2 →
+fact csx_appl_theta_aux: â\88\80h,o,p,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â¬\86*[1] V1 â\89\98 V2 →
                          ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
 #h #o #p #G #L #X #H @(csx_ind_cpxs … H) -X
 #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
@@ -95,5 +95,5 @@ elim (cpx_inv_appl1 … HL) -HL *
 qed-.
 
 lemma csx_appl_theta: ∀h,o,p,G,L,V,V2,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
-                      â\88\80V1. â¬\86*[1] V1 â\89¡ V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+                      â\88\80V1. â¬\86*[1] V1 â\89\98 V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
 /2 width=5 by csx_appl_theta_aux/ qed.