fact: Definition vec_decomp n (v : vec n) := match v in Vector.t _ k return vec_decomp_type k with | vec_nil => False | x ## v => (x,v) end.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)