X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_uni.ma;h=fa8cf7ebfa3d955e47ad2e36d40c00f214feb4d8;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=247311b3ed0359a5f159effbfa052172383b960d;hpb=75f395f0febd02de8e0f881d918a8812b1425c8d;p=helm.git

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 247311b3e..fa8cf7ebf 100644
--- 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 ⇒ ⫯(uni n)
+| S n ⇒ ↑(uni n)
 ].
 
 interpretation "uniform relocation (rtmap)"
@@ -28,74 +28,74 @@ interpretation "uniform relocation (rtmap)"
 
 (* Basic properties *********************************************************)
 
-lemma uni_zero: 𝐈𝐝 = 𝐔❴0❵.
+lemma uni_zero: 𝐈𝐝 = 𝐔❨0❩.
 // qed.
 
-lemma uni_succ: ∀n. ⫯𝐔❴n❵ = 𝐔❴⫯n❵.
+lemma uni_succ: ∀n. ↑𝐔❨n❩ = 𝐔❨↑n❩.
 // qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma uni_inv_push_dx: ∀f,n. 𝐔❴n❵ ≗ ↑f → 0 = n ∧ 𝐈𝐝 ≗ f.
+lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯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: ∀f,n. ↑f ≗ 𝐔❴n❵ → 0 = n ∧ 𝐈𝐝 ≗ f.
+lemma uni_inv_push_sn: ∀f,n. ⫯f ≡ 𝐔❨n❩ → 0 = n ∧ 𝐈𝐝 ≡ f.
 /3 width=1 by uni_inv_push_dx, eq_sym/ qed-.
 
-lemma uni_inv_id_dx: ∀n. 𝐔❴n❵ ≗ 𝐈𝐝 → 0 = n.
+lemma uni_inv_id_dx: ∀n. 𝐔❨n❩ ≡ 𝐈𝐝 → 0 = n.
 #n <id_rew #H elim (uni_inv_push_dx … H) -H //
 qed-.
 
-lemma uni_inv_id_sn: ∀n.  𝐈𝐝 ≗ 𝐔❴n❵ → 0 = n.
+lemma uni_inv_id_sn: ∀n.  𝐈𝐝 ≡ 𝐔❨n❩ → 0 = n.
 /3 width=1 by uni_inv_id_dx, eq_sym/ qed-.
 
-lemma uni_inv_next_dx: ∀f,n. 𝐔❴n❵ ≗ ⫯f → ∃∃m. 𝐔❴m❵ ≗ f & ⫯m = n.
+lemma uni_inv_next_dx: ∀f,n. 𝐔❨n❩ ≡ ↑f → ∃∃m. 𝐔❨m❩ ≡ 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: ∀f,n. ⫯f ≗ 𝐔❴n❵ → ∃∃m. 𝐔❴m❵ ≗ f & ⫯m = n.
+lemma uni_inv_next_sn: ∀f,n. ↑f ≡ 𝐔❨n❩ → ∃∃m. 𝐔❨m❩ ≡ f & ↑m = n.
 /3 width=1 by uni_inv_next_dx, eq_sym/ qed-.
 
 (* Properties with test for identity ****************************************)
 
-lemma uni_isid: ∀f. 𝐈⦃f⦄ → 𝐔❴0❵ ≗ f.
+lemma uni_isid: ∀f. 𝐈❪f❫ → 𝐔❨0❩ ≡ f.
 /2 width=1 by eq_id_inv_isid/ qed-.
 
 (* Inversion lemmas with test for identity **********************************)
 
-lemma uni_inv_isid: ∀f. 𝐔❴0❵ ≗ f → 𝐈⦃f⦄.
+lemma uni_inv_isid: ∀f. 𝐔❨0❩ ≡ f → 𝐈❪f❫.
 /2 width=1 by eq_id_isid/ qed-.
 
 (* Properties with finite colength assignment ***************************)
 
-lemma fcla_uni: ∀n. 𝐂⦃𝐔❴n❵⦄ ≘ n.
+lemma fcla_uni: ∀n. 𝐂❪𝐔❨n❩❫ ≘ n.
 #n elim n -n /2 width=1 by fcla_isid, fcla_next/
 qed.
 
 (* Properties with test for finite colength ***************************)
 
-lemma isfin_uni: ∀n. 𝐅⦃𝐔❴n❵⦄.
+lemma isfin_uni: ∀n. 𝐅❪𝐔❨n❩❫.
 /3 width=2 by ex_intro/ qed.
 
 (* Properties with test for uniformity **************************************)
 
-lemma isuni_uni: ∀n. 𝐔⦃𝐔❴n❵⦄.
+lemma isuni_uni: ∀n. 𝐔❪𝐔❨n❩❫.
 #n elim n -n /3 width=3 by isuni_isid, isuni_next/
 qed.
 
-lemma uni_isuni: ∀f. 𝐔⦃f⦄ → ∃n. 𝐔❴n❵ ≗ f.
+lemma uni_isuni: ∀f. 𝐔❪f❫ → ∃n. 𝐔❨n❩ ≡ 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: ∀n,f. 𝐔❴n❵ ≗ f →  𝐔⦃f⦄.
+lemma uni_inv_isuni: ∀n,f. 𝐔❨n❩ ≡ 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-.