proposition: Fact list_has_dup_cons_iff x l : list_has_dup (x::l) <-> In x l \/ list_has_dup l.
proof: Proof. split. + apply list_hd_cons_inv. + intros []; [ constructor 1 | constructor 2 ]; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)