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

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 a60ba3956..a4f7bb851 100644
--- 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: ∀i. minuss i (⟠) (⟠)
+| minuss_nil: ∀i. minuss i (◊) (◊)
 | 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: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠.
+fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ◊ → des2 = ◊.
 #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: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠.
+lemma minuss_inv_nil1: ∀des2,i. ◊ ▭ i ≡ des2 → des2 = ◊.
 /2 width=4 by minuss_inv_nil1_aux/ qed-.
 
 fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →