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