update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma
index 82c1b2f63832583ca1031278450c0945ae078265..af1ef01587479de54175aea63515549c2d7b2ed5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_computation/fpbg_fqup.ma".
 (* Properties with t-bound rt-transition for terms **************************)
 
 lemma cpm_tneqx_cpm_fpbg (h) (G) (L):
-      â\88\80n1,T1,T. â\9dªG,Lâ\9d« ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) →
-      â\88\80n2,T2. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n2] T2 â\86\92 â\9dªG,L,T1â\9d« > â\9dªG,L,T2â\9d«.
+      â\88\80n1,T1,T. â\9d¨G,Lâ\9d© ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) →
+      â\88\80n2,T2. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡[h,n2] T2 â\86\92 â\9d¨G,L,T1â\9d© > â\9d¨G,L,T2â\9d©.
 /4 width=5 by fpbc_fpbs_fpbg, fpb_fpbs, cpm_fwd_fpbc, cpm_fwd_fpb/
 qed.