update in ground_2, static_2, basic_2, apps_2, alpha_1

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

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 b0dc5e24f2d5c4e83eb2c10411d889f7ac4ba65d..ff61d6fb23c53516e87276f3fc9351ae69f5a3da 100644 (file)
--- 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 â\86\92 nat â\86\92 rtmap â\89\9d λm,n. ⫯*[m] ð\9d\90\94â\9d´nâ\9dµ.
+definition basic: nat â\86\92 nat â\86\92 rtmap â\89\9d λm,n. ⫯*[m] ð\9d\90\94â\9d¨nâ\9d©.
 
 interpretation "basic relocation (rtmap)"
    'Basic m n = (basic m n).
 
 (* Prioerties with application **********************************************)
 
-lemma at_basic_lt: â\88\80m,n,i. i < m â\86\92 @â¦\83i, ð\9d\90\81â\9d´m,nâ\9dµâ¦\84 ≘ i.
+lemma at_basic_lt: â\88\80m,n,i. i < m â\86\92 @â\9dªi, ð\9d\90\81â\9d¨m,nâ\9d©â\9d« ≘ 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: â\88\80m,n,i. m â\89¤ i â\86\92 @â¦\83i, ð\9d\90\81â\9d´m,nâ\9dµâ¦\84 ≘ n+i.
+lemma at_basic_ge: â\88\80m,n,i. m â\89¤ i â\86\92 @â\9dªi, ð\9d\90\81â\9d¨m,nâ\9d©â\9d« ≘ 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: â\88\80m,n,i,j. i < m â\86\92 @â¦\83i, ð\9d\90\81â\9d´m,nâ\9dµâ¦\84 ≘ j → i = j.
+lemma at_basic_inv_lt: â\88\80m,n,i,j. i < m â\86\92 @â\9dªi, ð\9d\90\81â\9d¨m,nâ\9d©â\9d« ≘ j → i = j.
 /3 width=4 by at_basic_lt, at_mono/ qed-.
 
-lemma at_basic_inv_ge: â\88\80m,n,i,j. m â\89¤ i â\86\92 @â¦\83i, ð\9d\90\81â\9d´m,nâ\9dµâ¦\84 ≘ j → n+i = j.
+lemma at_basic_inv_ge: â\88\80m,n,i,j. m â\89¤ i â\86\92 @â\9dªi, ð\9d\90\81â\9d¨m,nâ\9d©â\9d« ≘ j → n+i = j.
 /3 width=4 by at_basic_ge, at_mono/ qed-.