fact: Fixpoint vec_map n (v : vec X n) := match v with | vec_nil => vec_nil | x ## v => f x ## vec_map v end.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)