X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fmr2.ma;h=137c179fa9c1f3e0e5c817730d62fbdea073d33d;hb=d6909ee6f43e0f29efbaf28b75b69723634c3af2;hp=bf4331b89ce5880b92f599feb69cfbd647ef4334;hpb=886d7c4b7a21b4ca8f148d42555a5d89e8222fc8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma
index bf4331b89..137c179fa 100644
--- 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: ∀i. at (⟠) i i
+| at_nil: ∀i. at (◊) 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: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2.
+fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ◊ → 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: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2.
+lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2.
 /2 width=3 by at_inv_nil_aux/ qed-.
 
 fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →