- advances in the theory of cofrees

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lsx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
index 435650bd1577b568851819f9f9fc4c564fcd0ec0..0f47fe0567f69a3b5725c48bbc6e25fa3ad80500 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
@@ -29,7 +29,7 @@ interpretation
 
 lemma lsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv.
                (∀L1. G ⊢ ⬊*[h, g, T, d] L1 →
-                     (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\8b\95[T, d] L2 → ⊥) → R L2) →
+                     (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\89¡[T, d] L2 → ⊥) → R L2) →
                      R L1
                ) →
                ∀L. G ⊢ ⬊*[h, g, T, d] L → R L.
@@ -40,7 +40,7 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma lsx_intro: ∀h,g,G,L1,T,d.
-                 (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\8b\95[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) →
+                 (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\89¡[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) →
                  G ⊢ ⬊*[h, g, T, d] L1.
 /5 width=1 by lleq_sym, SN_intro/ qed.