proposition: Fact list_vec_iso l : vec_list (list_vec l) = l.
proof: Proof. induction l; simpl; f_equal; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)