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)"
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 ***************************)
#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-.