update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / fpb_feqg.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma
index 22219566dbf428ddf17fd741534dd3dc8a9b00e7..73c82b8b1270a07a83a8c4778ff7eeb84ccc0161 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma
@@ -26,7 +26,7 @@ include "basic_2/rt_transition/fpb.ma".
 (* Basic_2A1: uses: fpbq_feqx *)
 lemma feqg_fpb (S) (G1) (G2) (L1) (L2) (T1) (T2):
       reflexive … S → symmetric … S →
-      â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d«.
+      â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d©.
 #S #G1 #G2 #L1 #L2 #T1 #T2 #HS1 #HS2 #H
 elim (feqg_inv_gen_sn … H) -H #H #HL12 #HT12 destruct
 /4 width=8 by reqg_rpx, teqg_cpx, fpb_intro/
@@ -34,8 +34,8 @@ qed.
 
 lemma feqg_fpb_trans (S) (G) (L) (T):
       reflexive … S → symmetric … S → Transitive … S →
-      â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« â\89\9b[S] â\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« â\89½ â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\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© â\89½ â\9d¨G2,L2,T2â\9d©.
 #S #G #L #T #H1S #H2S #H3S #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
 elim (fpb_inv_gen … H2) -H2 #L0 #T0 #H0 #HT02 #H
 elim (rpx_inv_reqg_lpx S … H) -H // #L3 #HL03 #HL32