--- /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_2/notation/relations/rcolength_2.ma".
+include "ground_2/relocation/rtmap_isid.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+inductive fcla: relation2 rtmap nat ā
+| fcla_isid: āf. šā¦f⦠ā fcla f 0
+| fcla_push: āf,n. fcla f n ā fcla (āf) n
+| fcla_next: āf,n. fcla f n ā fcla (⫯f) (⫯n)
+.
+
+interpretation "finite colength assignment (rtmap)"
+ 'RCoLength f n = (fcla f n).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fcla_inv_px: āg,m. šā¦g⦠┠m ā āf. āf = g ā šā¦f⦠┠m.
+#g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/
+#g #m #_ #f #H elim (discr_push_next ⦠H)
+qed-.
+
+lemma fcla_inv_nx: āg,m. šā¦g⦠┠m ā āf. ⫯f = g ā
+ āān. šā¦f⦠┠n & ⫯n = m.
+#g #m * -g -m /2 width=3 by ex2_intro/
+[ #g #Hg #f #H elim (isid_inv_next ⦠H) -H //
+| #g #m #_ #f #H elim (discr_next_push ⦠H)
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cla_inv_nn: āg,m. šā¦g⦠┠m ā āf,n. ⫯f = g ā ⫯n = m ā šā¦f⦠┠n.
+#g #m #H #f #n #H1 #H2 elim (fcla_inv_nx ⦠H ⦠H1) -g
+#x #Hf #H destruct //
+qed-.
+
+lemma cla_inv_np: āg,m. šā¦g⦠┠m ā āf. ⫯f = g ā 0 = m ā ā„.
+#g #m #H #f #H1 elim (fcla_inv_nx ⦠H ⦠H1) -g
+#x #_ #H1 #H2 destruct
+qed-.
+
+lemma fcla_inv_xp: āg,m. šā¦g⦠┠m ā 0 = m ā šā¦gā¦.
+#g #m #H elim H -g -m /3 width=3 by isid_push/
+#g #m #_ #_ #H destruct
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fcla_eq_repl_back: ān. eq_repl_back ⦠(Ī»f. šā¦f⦠┠n).
+#n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
+#f1 #n #_ #IH #g2 #H [ elim (eq_inv_px ⦠H) | elim (eq_inv_nx ⦠H) ] -H
+/3 width=3 by fcla_push, fcla_next/
+qed-.
+
+lemma fcla_eq_repl_fwd: ān. eq_repl_fwd ⦠(Ī»f. šā¦f⦠┠n).
+#n @eq_repl_sym /2 width=3 by fcla_eq_repl_back/
+qed-.