fact: Fixpoint in_vec n (v : vec n) : Prop := match v with | vec_nil => False | y ## v => y = x \/ in_vec v end.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)