include "ground_2/relocation/rtmap_eq.ma".
(* RELOCATION MAP ***********************************************************)
rec definition nexts (f:rtmap) (n:nat) on n: rtmap ≝ match n with
include "ground_2/relocation/rtmap_eq.ma".
(* RELOCATION MAP ***********************************************************)
rec definition nexts (f:rtmap) (n:nat) on n: rtmap ≝ match n with