fact: Fixpoint vec_map_list X n v : (pos n -> X) -> list X := match v in vec _ m return (pos m -> _) -> _ with | vec_nil => fun _ => nil | a##v => fun f => list_repeat (f pos0) a ++ vec_map_list v (fun p => f (pos_nxt p)) end.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)