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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma
index 613f27991..12e2cfdda 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma
@@ -19,16 +19,16 @@ include "ground_2/relocation/nstream_after.ma".
 
 (* Specific properties on basic relocation **********************************)
 
-lemma apply_basic_lt: ∀m,n,i. i < m → 𝐁❴m,n❵@❴i❵ = i.
+lemma apply_basic_lt: ∀m,n,i. i < m → 𝐁❨m,n❩@❨i❩ = i.
 /3 width=1 by at_inv_total, at_basic_lt/ qed-.
 
-lemma apply_basic_ge: ∀m,n,i. m ≤ i → 𝐁❴m,n❵@❴i❵ = n+i.
+lemma apply_basic_ge: ∀m,n,i. m ≤ i → 𝐁❨m,n❩@❨i❩ = n+i.
 /3 width=1 by at_inv_total, at_basic_ge/ qed-.
 
 (* Specific main properties on basic relocation *****************************)
 
 theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
-                    ∀h1,h2. 𝐁❴d2,h2❵∘𝐁❴d1,h1❵ ≡ 𝐁❴h2+d1,h1❵∘𝐁❴d2,h2❵.
+                    ∀h1,h2. 𝐁❨d2,h2❩∘𝐁❨d1,h1❩ ≡ 𝐁❨h2+d1,h1❩∘𝐁❨d2,h2❩.
 #d1 #d2 #Hd21 #h1 #h2
 @nstream_inv_eq
 @nstream_eq_inv_ext #i