proposition: Fact vec_list_length n v : length (@vec_list n v) = n.
proof: Proof. induction v; simpl; f_equal; auto. Defined.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)