update in static_2

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

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 13db8d1f3a1c9f74e48deedad6e9d6f73ea2091f..437457f659dc964c076482e3e70ee7f66322b235 100644 (file)
--- 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 →
-        (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88 T2 â\86\92 (T1 â\89\9b T2 → ⊥) → Q T2) →
+        (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88 T2 â\86\92 (T1 â\89\85 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):
-      â\88\80T1. (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88 T2 â\86\92 (T1 â\89\9b T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒 T2) →
+      â\88\80T1. (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88 T2 â\86\92 (T1 â\89\85 T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒 T2) →
       ❪G,L❫ ⊢ ⬈*𝐒 T1.
 /4 width=1 by SN_intro/ qed.