update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream_basic.ma

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 613f279914cc532ffae198bb340ac7bc17e13b17..12e2cfdda28ad4934ef3be9f255e6cf8c0382609 100644 (file)
--- 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: â\88\80m,n,i. i < m â\86\92 ð\9d\90\81â\9d´m,nâ\9dµ@â\9d´iâ\9dµ = i.
+lemma apply_basic_lt: â\88\80m,n,i. i < m â\86\92 ð\9d\90\81â\9d¨m,nâ\9d©@â\9d¨iâ\9d© = i.
 /3 width=1 by at_inv_total, at_basic_lt/ qed-.
 
-lemma apply_basic_ge: â\88\80m,n,i. m â\89¤ i â\86\92 ð\9d\90\81â\9d´m,nâ\9dµ@â\9d´iâ\9dµ = n+i.
+lemma apply_basic_ge: â\88\80m,n,i. m â\89¤ i â\86\92 ð\9d\90\81â\9d¨m,nâ\9d©@â\9d¨iâ\9d© = 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 →
-                    â\88\80h1,h2. ð\9d\90\81â\9d´d2,h2â\9dµâ\88\98ð\9d\90\81â\9d´d1,h1â\9dµ â\89¡ ð\9d\90\81â\9d´h2+d1,h1â\9dµâ\88\98ð\9d\90\81â\9d´d2,h2â\9dµ.
+                    â\88\80h1,h2. ð\9d\90\81â\9d¨d2,h2â\9d©â\88\98ð\9d\90\81â\9d¨d1,h1â\9d© â\89¡ ð\9d\90\81â\9d¨h2+d1,h1â\9d©â\88\98ð\9d\90\81â\9d¨d2,h2â\9d©.
 #d1 #d2 #Hd21 #h1 #h2
 @nstream_inv_eq
 @nstream_eq_inv_ext #i