update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqg.ma
index 860aea3b54ee15eccc0ba2bf2cb386b67945a846..359e4228fce0db12c9610d171a294cf259cf5c3e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqg.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_computation/cpxs.ma".
 
 lemma teqg_cpxs_trans (S) (G) (L) (T):
       reflexive … S → symmetric … S →
-      â\88\80T1. T1 â\89\9b[S] T â\86\92 â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T â¬\88* T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬈* T2.
+      â\88\80T1. T1 â\89\9b[S] T â\86\92 â\88\80T2. â\9d¨G,Lâ\9d© â\8a¢ T â¬\88* T2 â\86\92 â\9d¨G,Lâ\9d© ⊢ T1 ⬈* T2.
 #S #H1S #H2S #G #L #T #T1 #HT1 #T2 #HT2 @(cpxs_ind … HT2) -T2
 [ /3 width=4 by teqg_cpx, cpx_cpxs/
 | /2 width=3 by cpxs_strap1/
@@ -33,8 +33,8 @@ qed-.
 lemma cpxs_tneqg_fwd_step_sn (S) (G) (L):
       reflexive … S → symmetric … S → Transitive … S →
       (∀s1,s2. Decidable (S s1 s2)) →
-      â\88\80T1,T2. â\9dªG,Lâ\9d« ⊢ T1 ⬈* T2 → (T1 ≛[S] T2 → ⊥) →
-      â\88\83â\88\83T. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88 T & T1 â\89\9b[S] T â\86\92 â\8a¥ & â\9dªG,Lâ\9d« ⊢ T ⬈* T2.
+      â\88\80T1,T2. â\9d¨G,Lâ\9d© ⊢ T1 ⬈* T2 → (T1 ≛[S] T2 → ⊥) →
+      â\88\83â\88\83T. â\9d¨G,Lâ\9d© â\8a¢ T1 â¬\88 T & T1 â\89\9b[S] T â\86\92 â\8a¥ & â\9d¨G,Lâ\9d© ⊢ T ⬈* T2.
 #S #G #L #H1S #H2S #H3S #H4S #T1 #T2 #H @(cpxs_ind_dx … H) -T1
 [ #H elim H -H /2 width=1 by teqg_refl/
 | #T1 #T0 #HT10 #HT02 #IH #HnT12