(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with