proposition: Fact vec_map_list_zero n f : vec_map_list (@vec_zero n) f = @nil X.
proof: Proof. revert f; induction n; intros f; simpl; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)