update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqus.ma
index 1c64f5eb254a266cf13bc62abf54c42da2685cec..fea456d482a46e3fafe744ae1580086057ef0ccc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqus.ma
@@ -24,13 +24,13 @@ include "basic_2/rt_computation/fpbg_fpbs.ma".
 
 (* Note: this is used in the closure proof *)
 lemma fqup_fpbg:
-      â\88\80G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82+ â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82+ â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
 /3 width=5 by fpbc_fpbs_fpbg, fqus_fpbs, fqu_fpbc/
 qed.
 
 (* Note: this is used in the closure proof *)
 lemma fqup_fpbg_trans (G) (L) (T):
-      â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« â¬\82+ â\9dªG,L,Tâ\9d« →
-      â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« > â\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© â¬\82+ â\9d¨G,L,Tâ\9d© →
+      â\88\80G2,L2,T2. â\9d¨G,L,Tâ\9d© > â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 /3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-.