update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
index 37681f1fa5ce4a0d3966880f3b5594edf7ef2dfe..3660f103c9385fadd72c28d5a3df8bda44e73a49 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
@@ -20,10 +20,10 @@ include "basic_2/rt_computation/fpbg.ma".
 (* Advanced properties ******************************************************)
 
 lemma fpbc_fpbg (G1) (G2) (L1) (L2) (T1) (T2):
-      â\9dªG1,L1,T1â\9d« â\89» â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+      â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 /3 width=13 by fpbg_intro, fpb_fpbs/ qed.
 
 lemma fpbc_fpbs_fpbg (G) (L) (T):
-      â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« â\89» â\9dªG,L,Tâ\9d« →
-      â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« â\89¥ â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G,L,Tâ\9d© →
+      â\88\80G2,L2,T2. â\9d¨G,L,Tâ\9d© â\89¥ â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 /2 width=9 by fpbg_intro/ qed.