bug fix in ththe notation for lists:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / mr2.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma
index bf4331b89ce5880b92f599feb69cfbd647ef4334..137c179fa9c1f3e0e5c817730d62fbdea073d33d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma
@@ -18,7 +18,7 @@ include "basic_2/grammar/term_vector.ma".
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 
 inductive at: list2 nat nat → relation nat ≝
-| at_nil: â\88\80i. at (â\9f ) i i
+| at_nil: â\88\80i. at (â\97\8a) i i
 | at_lt : ∀des,d,e,i1,i2. i1 < d →
           at des i1 i2 → at ({d, e} @ des) i1 i2
 | at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
@@ -30,7 +30,7 @@ interpretation "application (multiple relocation with pairs)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact at_inv_nil_aux: â\88\80des,i1,i2. @â¦\83i1, desâ¦\84 â\89¡ i2 â\86\92 des = â\9f  → i1 = i2.
+fact at_inv_nil_aux: â\88\80des,i1,i2. @â¦\83i1, desâ¦\84 â\89¡ i2 â\86\92 des = â\97\8a → i1 = i2.
 #des #i1 #i2 * -des -i1 -i2
 [ //
 | #des #d #e #i1 #i2 #_ #_ #H destruct
@@ -38,7 +38,7 @@ fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 =
 ]
 qed-.
 
-lemma at_inv_nil: â\88\80i1,i2. @â¦\83i1, â\9f ⦄ ≡ i2 → i1 = i2.
+lemma at_inv_nil: â\88\80i1,i2. @â¦\83i1, â\97\8a⦄ ≡ i2 → i1 = i2.
 /2 width=3 by at_inv_nil_aux/ qed-.
 
 fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →