update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
index a1ac691824c89bc946a8a9fc477a1f216c2cc6f1..5a981f8e2b01ebd65c226910a43c68dfd84ae368 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_computation/fpbg.ma".
 (* Advanced forward lemmas **************************************************)
 
 lemma fpbg_fwd_fpbs (G1) (G2) (L1) (L2) (T1) (T2):
-      â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d«.
+      â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d©.
 #G1 #G2 #L1 #L2 #T1 #T2 #H
 elim (fpbg_inv_gen … H) -H
 /4 width=9 by fpbs_trans, fpbs_strap2, fpbc_fwd_fpb/
@@ -29,8 +29,8 @@ qed-.
 (* Advanced properties ******************************************************)
 
 lemma fpbs_fpbg_trans (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« > â\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© > â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 #G #L #T #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
 elim (fpbg_inv_gen … H2) -H2
 /3 width=13 by fpbg_intro, fpbs_trans/
@@ -38,8 +38,8 @@ qed-.
 
 (* Note: this is used in the closure proof *)
 lemma fpbg_fpbs_trans (G) (L) (T):
-      â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« > â\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© > â\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©.
 #G #L #T #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
 elim (fpbg_inv_gen … H1) -H1
 /3 width=13 by fpbg_intro, fpbs_trans/