X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_uni.ma;h=bacac08bfa7177cf92d9993e291023dc27669367;hb=54c4e854515cbcb1376881e9aedad006bf6545f2;hp=5f45b1f2889ff777a82f174b8e262e402cd591b7;hpb=9a023f554e56d6edbbb2eeaf17ce61e31857ef4a;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 5f45b1f28..bacac08bf 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)"
@@ -31,49 +31,49 @@ interpretation "uniform relocation (rtmap)"
 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.
 
@@ -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: ∀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-.