update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqg.ma
index ea40d9b708c45fcb4ce3eb06969f02c6290a339d..f89db09594cefaf9a98944022dc2ff89e09a31da 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqg.ma
@@ -22,8 +22,8 @@ include "basic_2/rt_computation/csx_csx.ma".
 (* Basic_2A1: uses: csx_lleq_conf *)
 lemma csx_reqg_conf (S) (G) (T):
       reflexive … S → symmetric … S →
-      â\88\80L1. â\9dªG,L1â\9d« ⊢ ⬈*𝐒 T →
-      â\88\80L2. L1 â\89\9b[S,T] L2 â\86\92 â\9dªG,L2â\9d« ⊢ ⬈*𝐒 T.
+      â\88\80L1. â\9d¨G,L1â\9d© ⊢ ⬈*𝐒 T →
+      â\88\80L2. L1 â\89\9b[S,T] L2 â\86\92 â\9d¨G,L2â\9d© ⊢ ⬈*𝐒 T.
 #S #G #T #H1S #H2S #L1 #H
 @(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
 @csx_intro #T2 #HT12 #HnT12
@@ -34,5 +34,5 @@ qed-.
 (* Basic_2A1: uses: csx_lleq_trans *)
 lemma csx_reqg_trans (S) (G) (T):
       reflexive … S → symmetric … S →
-      â\88\80L1,L2. L1 â\89\9b[S,T] L2 â\86\92 â\9dªG,L2â\9d« â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\9dªG,L1â\9d« ⊢ ⬈*𝐒 T.
+      â\88\80L1,L2. L1 â\89\9b[S,T] L2 â\86\92 â\9d¨G,L2â\9d© â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈*𝐒 T.
 /3 width=8 by csx_reqg_conf, reqg_sym/ qed-.