bug fix in ththe notation for lists:

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma
index d589181eef620eb320c33026b09093957e19ffd9..6528fb827fb9ead0f1a3e795f3d5120cbbb89e7d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma
@@ -17,7 +17,7 @@ include "basic_2/multiple/mr2.ma".
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 
 let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
-[ nil2          â\87\92 â\9f 
+[ nil2          â\87\92 â\97\8a
 | cons2 d e des ⇒ {d + i, e} @ pluss des i
 ].
 
@@ -26,7 +26,7 @@ interpretation "plus (multiple relocation with pairs)"
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma pluss_inv_nil2: â\88\80i,des. des + i = â\9f  â\86\92 des = â\9f .
+lemma pluss_inv_nil2: â\88\80i,des. des + i = â\97\8a â\86\92 des = â\97\8a.
 #i * // normalize
 #d #e #des #H destruct
 qed.