update in ground_2, static_2, basic_2, apps_2, alpha_1

[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 bacac08bfa7177cf92d9993e291023dc27669367..fa8cf7ebfa3d955e47ad2e36d40c00f214feb4d8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
@@ -28,74 +28,74 @@ interpretation "uniform relocation (rtmap)"
 
 (* Basic properties *********************************************************)
 
-lemma uni_zero: ð\9d\90\88ð\9d\90\9d = ð\9d\90\94â\9d´0â\9dµ.
+lemma uni_zero: ð\9d\90\88ð\9d\90\9d = ð\9d\90\94â\9d¨0â\9d©.
 // qed.
 
-lemma uni_succ: â\88\80n. â\86\91ð\9d\90\94â\9d´nâ\9dµ = ð\9d\90\94â\9d´â\86\91nâ\9dµ.
+lemma uni_succ: â\88\80n. â\86\91ð\9d\90\94â\9d¨nâ\9d© = ð\9d\90\94â\9d¨â\86\91nâ\9d©.
 // qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma uni_inv_push_dx: â\88\80f,n. ð\9d\90\94â\9d´nâ\9dµ ≡ ⫯f → 0 = n ∧ 𝐈𝐝 ≡ f.
+lemma uni_inv_push_dx: â\88\80f,n. ð\9d\90\94â\9d¨nâ\9d© ≡ ⫯f → 0 = n ∧ 𝐈𝐝 ≡ 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. ⫯f â\89¡ ð\9d\90\94â\9d´nâ\9dµ → 0 = n ∧ 𝐈𝐝 ≡ f.
+lemma uni_inv_push_sn: â\88\80f,n. ⫯f â\89¡ ð\9d\90\94â\9d¨nâ\9d© → 0 = n ∧ 𝐈𝐝 ≡ 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µ ≡ 𝐈𝐝 → 0 = n.
+lemma uni_inv_id_dx: â\88\80n. ð\9d\90\94â\9d¨nâ\9d© ≡ 𝐈𝐝 → 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¡ ð\9d\90\94â\9d´nâ\9dµ → 0 = n.
+lemma uni_inv_id_sn: â\88\80n.  ð\9d\90\88ð\9d\90\9d â\89¡ ð\9d\90\94â\9d¨nâ\9d© → 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¡ â\86\91f â\86\92 â\88\83â\88\83m. ð\9d\90\94â\9d´mâ\9dµ ≡ 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© ≡ f & ↑m = 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. â\86\91f â\89¡ ð\9d\90\94â\9d´nâ\9dµ â\86\92 â\88\83â\88\83m. ð\9d\90\94â\9d´mâ\9dµ ≡ 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© ≡ f & ↑m = 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µ ≡ f.
+lemma uni_isid: â\88\80f. ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\94â\9d¨0â\9d© ≡ 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¡ f â\86\92 ð\9d\90\88â¦\83fâ¦\84.
+lemma uni_inv_isid: â\88\80f. ð\9d\90\94â\9d¨0â\9d© â\89¡ f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
 /2 width=1 by eq_id_isid/ qed-.
 
 (* Properties with finite colength assignment ***************************)
 
-lemma fcla_uni: â\88\80n. ð\9d\90\82â¦\83ð\9d\90\94â\9d´nâ\9dµâ¦\84 ≘ n.
+lemma fcla_uni: â\88\80n. ð\9d\90\82â\9dªð\9d\90\94â\9d¨nâ\9d©â\9d« ≘ n.
 #n elim n -n /2 width=1 by fcla_isid, fcla_next/
 qed.
 
 (* Properties with test for finite colength ***************************)
 
-lemma isfin_uni: â\88\80n. ð\9d\90\85â¦\83ð\9d\90\94â\9d´nâ\9dµâ¦\84.
+lemma isfin_uni: â\88\80n. ð\9d\90\85â\9dªð\9d\90\94â\9d¨nâ\9d©â\9d«.
 /3 width=2 by ex_intro/ qed.
 
 (* Properties with test for uniformity **************************************)
 
-lemma isuni_uni: â\88\80n. ð\9d\90\94â¦\83ð\9d\90\94â\9d´nâ\9dµâ¦\84.
+lemma isuni_uni: â\88\80n. ð\9d\90\94â\9dªð\9d\90\94â\9d¨nâ\9d©â\9d«.
 #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µ ≡ f.
+lemma uni_isuni: â\88\80f. ð\9d\90\94â\9dªfâ\9d« â\86\92 â\88\83n. ð\9d\90\94â\9d¨nâ\9d© ≡ 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¡ f â\86\92  ð\9d\90\94â¦\83fâ¦\84.
+lemma uni_inv_isuni: â\88\80n,f. ð\9d\90\94â\9d¨nâ\9d© â\89¡ f â\86\92  ð\9d\90\94â\9dªfâ\9d«.
 #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-.