proposition: Fact list_has_dup_app_left l m : list_has_dup m -> list_has_dup (l++m).
proof: Proof. induction l; simpl; auto; constructor 2; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)