syntactic components detached from basic_2 become static_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
index 247311b3ed0359a5f159effbfa052172383b960d..bacac08bfa7177cf92d9993e291023dc27669367 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
@@ -20,7 +20,7 @@ include "ground_2/relocation/rtmap_isuni.ma".
 
 rec definition uni (n:nat) on n: rtmap  ≝ match n with
 [ O   ⇒ 𝐈𝐝
-| S n â\87\92 ⫯(uni n)
+| S n â\87\92 â\86\91(uni n)
 ].
 
 interpretation "uniform relocation (rtmap)"
@@ -31,44 +31,44 @@ interpretation "uniform relocation (rtmap)"
 lemma uni_zero: 𝐈𝐝 = 𝐔❴0❵.
 // qed.
 
-lemma uni_succ: â\88\80n. ⫯ð\9d\90\94â\9d´nâ\9dµ = ð\9d\90\94â\9d´â«¯n❵.
+lemma uni_succ: â\88\80n. â\86\91ð\9d\90\94â\9d´nâ\9dµ = ð\9d\90\94â\9d´â\86\91n❵.
 // qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma uni_inv_push_dx: â\88\80f,n. ð\9d\90\94â\9d´nâ\9dµ â\89\97 â\86\91f â\86\92 0 = n â\88§ ð\9d\90\88ð\9d\90\9d â\89\97 f.
+lemma uni_inv_push_dx: â\88\80f,n. ð\9d\90\94â\9d´nâ\9dµ â\89¡ ⫯f â\86\92 0 = n â\88§ ð\9d\90\88ð\9d\90\9d â\89¡ f.
 #f * /3 width=5 by eq_inv_pp, conj/
 #n <uni_succ #H elim (eq_inv_np … H) -H //
 qed-.
 
-lemma uni_inv_push_sn: â\88\80f,n. â\86\91f â\89\97 ð\9d\90\94â\9d´nâ\9dµ â\86\92 0 = n â\88§ ð\9d\90\88ð\9d\90\9d â\89\97 f.
+lemma uni_inv_push_sn: â\88\80f,n. ⫯f â\89¡ ð\9d\90\94â\9d´nâ\9dµ â\86\92 0 = n â\88§ ð\9d\90\88ð\9d\90\9d â\89¡ f.
 /3 width=1 by uni_inv_push_dx, eq_sym/ qed-.
 
-lemma uni_inv_id_dx: â\88\80n. ð\9d\90\94â\9d´nâ\9dµ â\89\97 𝐈𝐝 → 0 = n.
+lemma uni_inv_id_dx: â\88\80n. ð\9d\90\94â\9d´nâ\9dµ â\89¡ 𝐈𝐝 → 0 = n.
 #n <id_rew #H elim (uni_inv_push_dx … H) -H //
 qed-.
 
-lemma uni_inv_id_sn: â\88\80n.  ð\9d\90\88ð\9d\90\9d â\89\97 𝐔❴n❵ → 0 = n.
+lemma uni_inv_id_sn: â\88\80n.  ð\9d\90\88ð\9d\90\9d â\89¡ 𝐔❴n❵ → 0 = n.
 /3 width=1 by uni_inv_id_dx, eq_sym/ qed-.
 
-lemma uni_inv_next_dx: â\88\80f,n. ð\9d\90\94â\9d´nâ\9dµ â\89\97 ⫯f â\86\92 â\88\83â\88\83m. ð\9d\90\94â\9d´mâ\9dµ â\89\97 f & ⫯m = n.
+lemma uni_inv_next_dx: â\88\80f,n. ð\9d\90\94â\9d´nâ\9dµ â\89¡ â\86\91f â\86\92 â\88\83â\88\83m. ð\9d\90\94â\9d´mâ\9dµ â\89¡ f & â\86\91m = n.
 #f *
 [ <uni_zero <id_rew #H elim (eq_inv_pn … H) -H //
 | #n <uni_succ /3 width=5 by eq_inv_nn, ex2_intro/
 ]
 qed-.
 
-lemma uni_inv_next_sn: â\88\80f,n. ⫯f â\89\97 ð\9d\90\94â\9d´nâ\9dµ â\86\92 â\88\83â\88\83m. ð\9d\90\94â\9d´mâ\9dµ â\89\97 f & ⫯m = n.
+lemma uni_inv_next_sn: â\88\80f,n. â\86\91f â\89¡ ð\9d\90\94â\9d´nâ\9dµ â\86\92 â\88\83â\88\83m. ð\9d\90\94â\9d´mâ\9dµ â\89¡ f & â\86\91m = n.
 /3 width=1 by uni_inv_next_dx, eq_sym/ qed-.
 
 (* Properties with test for identity ****************************************)
 
-lemma uni_isid: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 ð\9d\90\94â\9d´0â\9dµ â\89\97 f.
+lemma uni_isid: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 ð\9d\90\94â\9d´0â\9dµ â\89¡ f.
 /2 width=1 by eq_id_inv_isid/ qed-.
 
 (* Inversion lemmas with test for identity **********************************)
 
-lemma uni_inv_isid: â\88\80f. ð\9d\90\94â\9d´0â\9dµ â\89\97 f → 𝐈⦃f⦄.
+lemma uni_inv_isid: â\88\80f. ð\9d\90\94â\9d´0â\9dµ â\89¡ f → 𝐈⦃f⦄.
 /2 width=1 by eq_id_isid/ qed-.
 
 (* Properties with finite colength assignment ***************************)
@@ -88,14 +88,14 @@ lemma isuni_uni: ∀n. 𝐔⦃𝐔❴n❵⦄.
 #n elim n -n /3 width=3 by isuni_isid, isuni_next/
 qed.
 
-lemma uni_isuni: â\88\80f. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â\88\83n. ð\9d\90\94â\9d´nâ\9dµ â\89\97 f.
+lemma uni_isuni: â\88\80f. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â\88\83n. ð\9d\90\94â\9d´nâ\9dµ â\89¡ f.
 #f #H elim H -f /3 width=2 by uni_isid, ex_intro/
 #f #_ #g #H * /3 width=6 by eq_next, ex_intro/
 qed-.
 
 (* Inversion lemmas with test for uniformity ********************************)
 
-lemma uni_inv_isuni: â\88\80n,f. ð\9d\90\94â\9d´nâ\9dµ â\89\97 f →  𝐔⦃f⦄.
+lemma uni_inv_isuni: â\88\80n,f. ð\9d\90\94â\9d´nâ\9dµ â\89¡ f →  𝐔⦃f⦄.
 #n elim n -n /3 width=1 by uni_inv_isid, isuni_isid/
 #n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
 qed-.