proposition: Fact list_has_dup_swap x y l : list_has_dup (x::y::l) -> list_has_dup (y::x::l).
proof: Proof. apply perm_list_has_dup; constructor. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)