X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx.ma;h=437457f659dc964c076482e3e70ee7f66322b235;hp=13db8d1f3a1c9f74e48deedad6e9d6f73ea2091f;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hpb=613d8642b1154dde0c026cbdcd96568910198251

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
index 13db8d1f3..437457f65 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
@@ -29,7 +29,7 @@ interpretation
 
 lemma csx_ind (G) (L) (Q:predicate …):
       (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
-        (∀T2. ❪G,L❫ ⊢ T1 ⬈ T2 → (T1 ≛ T2 → ⊥) → Q T2) →
+        (∀T2. ❪G,L❫ ⊢ T1 ⬈ T2 → (T1 ≅ T2 → ⊥) → Q T2) →
         Q T1
       ) →
       ∀T. ❪G,L❫ ⊢ ⬈*𝐒 T →  Q T.
@@ -41,7 +41,7 @@ qed-.
 
 (* Basic_1: was just: sn3_pr2_intro *)
 lemma csx_intro (G) (L):
-      ∀T1. (∀T2. ❪G,L❫ ⊢ T1 ⬈ T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒 T2) →
+      ∀T1. (∀T2. ❪G,L❫ ⊢ T1 ⬈ T2 → (T1 ≅ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒 T2) →
       ❪G,L❫ ⊢ ⬈*𝐒 T1.
 /4 width=1 by SN_intro/ qed.