proposition: Fact list_hd_cons_inv x l : list_has_dup (x::l) -> In x l \/ list_has_dup l.
proof: Proof. inversion 1; subst; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)