bug fix in ththe notation for lists:

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma
index a60ba39564fdb038107ba5638425ce8607e1ff9a..a4f7bb85139a0b20934933f4e94f7178401a4df5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma
@@ -18,7 +18,7 @@ include "basic_2/multiple/mr2.ma".
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 
 inductive minuss: nat → relation (list2 nat nat) ≝
-| minuss_nil: â\88\80i. minuss i (â\9f ) (â\9f )
+| minuss_nil: â\88\80i. minuss i (â\97\8a) (â\97\8a)
 | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
               minuss i ({d, e} @ des1) ({d - i, e} @ des2)
 | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
@@ -30,7 +30,7 @@ interpretation "minus (multiple relocation with pairs)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact minuss_inv_nil1_aux: â\88\80des1,des2,i. des1 â\96­ i â\89¡ des2 â\86\92 des1 = â\9f  â\86\92 des2 = â\9f .
+fact minuss_inv_nil1_aux: â\88\80des1,des2,i. des1 â\96­ i â\89¡ des2 â\86\92 des1 = â\97\8a â\86\92 des2 = â\97\8a.
 #des1 #des2 #i * -des1 -des2 -i
 [ //
 | #des1 #des2 #d #e #i #_ #_ #H destruct
@@ -38,7 +38,7 @@ fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ →
 ]
 qed-.
 
-lemma minuss_inv_nil1: â\88\80des2,i. â\9f  â\96­ i â\89¡ des2 â\86\92 des2 = â\9f .
+lemma minuss_inv_nil1: â\88\80des2,i. â\97\8a â\96­ i â\89¡ des2 â\86\92 des2 = â\97\8a.
 /2 width=4 by minuss_inv_nil1_aux/ qed-.
 
 fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →