--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/notation/relations/isuniform_1.ma".
+include "ground/relocation/rtmap_isfin.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+inductive isuni: predicate rtmap ā
+| isuni_isid: āf. šāŖfā« ā isuni f
+| isuni_next: āf. isuni f ā āg. āf = g ā isuni g
+.
+
+interpretation "test for uniformity (rtmap)"
+ 'IsUniform f = (isuni f).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isuni_inv_push: āg. šāŖgā« ā āf. ā«Æf = g ā šāŖfā«.
+#g * -g /2 width=3 by isid_inv_push/
+#f #_ #g #H #x #Hx destruct elim (discr_push_next ā¦ Hx)
+qed-.
+
+lemma isuni_inv_next: āg. šāŖgā« ā āf. āf = g ā šāŖfā«.
+#g * -g #f #Hf
+[ #x #Hx elim (isid_inv_next ā¦ Hf ā¦ Hx)
+| #g #H #x #Hx destruct /2 width=1 by injective_push/
+]
+qed-.
+
+lemma isuni_split: āg. šāŖgā« ā (āāf. šāŖfā« & ā«Æf = g) āØ (āāf.šāŖfā« & āf = g).
+#g #H elim (pn_split g) * #f #Hf
+/4 width=3 by isuni_inv_next, isuni_inv_push, or_introl, or_intror, ex2_intro/
+qed-.
+
+(* basic forward lemmas *****************************************************)
+
+lemma isuni_fwd_push: āg. šāŖgā« ā āf. ā«Æf = g ā šāŖfā«.
+/3 width=3 by isuni_inv_push, isuni_isid/ qed-.
+
+(* Forward lemmas with test for finite colength *****************************)
+
+lemma isuni_fwd_isfin: āf. šāŖfā« ā š
āŖfā«.
+#f #H elim H -f /3 width=1 by isfin_next, isfin_isid/
+qed-.