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