fact: Fixpoint list_vec (l : list X) : vec (length l) := match l with | nil => vec_nil | x::l => x ## list_vec l end.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)