X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_basic.ma;h=ff61d6fb23c53516e87276f3fc9351ae69f5a3da;hp=b0dc5e24f2d5c4e83eb2c10411d889f7ac4ba65d;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma
index b0dc5e24f..ff61d6fb2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma
@@ -17,20 +17,20 @@ include "ground_2/relocation/rtmap_at.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
-definition basic: nat → nat → rtmap ≝ λm,n. ⫯*[m] 𝐔❴n❵.
+definition basic: nat → nat → rtmap ≝ λm,n. ⫯*[m] 𝐔❨n❩.
 
 interpretation "basic relocation (rtmap)"
    'Basic m n = (basic m n).
 
 (* Prioerties with application **********************************************)
 
-lemma at_basic_lt: ∀m,n,i. i < m → @⦃i, 𝐁❴m,n❵⦄ ≘ i.
+lemma at_basic_lt: ∀m,n,i. i < m → @❪i, 𝐁❨m,n❩❫ ≘ i.
 #m elim m -m [ #n #i #H elim (lt_zero_false … H) ]
 #m #IH #n * [ /2 width=2 by refl, at_refl/ ]
 #i #H lapply (lt_S_S_to_lt … H) -H /3 width=7 by refl, at_push/
 qed.
 
-lemma at_basic_ge: ∀m,n,i. m ≤ i → @⦃i, 𝐁❴m,n❵⦄ ≘ n+i.
+lemma at_basic_ge: ∀m,n,i. m ≤ i → @❪i, 𝐁❨m,n❩❫ ≘ n+i.
 #m elim m -m //
 #m #IH #n #j #H
 elim (le_inv_S1 … H) -H #i #Hmi #H destruct
@@ -39,8 +39,8 @@ qed.
 
 (* Inversion lemmas with application ****************************************)
 
-lemma at_basic_inv_lt: ∀m,n,i,j. i < m → @⦃i, 𝐁❴m,n❵⦄ ≘ j → i = j.
+lemma at_basic_inv_lt: ∀m,n,i,j. i < m → @❪i, 𝐁❨m,n❩❫ ≘ j → i = j.
 /3 width=4 by at_basic_lt, at_mono/ qed-.
 
-lemma at_basic_inv_ge: ∀m,n,i,j. m ≤ i → @⦃i, 𝐁❴m,n❵⦄ ≘ j → n+i = j.
+lemma at_basic_inv_ge: ∀m,n,i,j. m ≤ i → @❪i, 𝐁❨m,n❩❫ ≘ j → n+i = j.
 /3 width=4 by at_basic_ge, at_mono/ qed-.