proposition: Fact list_has_dup_eq_duplicates m: list_has_dup m <-> exists x aa bb cc, m = aa++x::bb++x::cc.
proof: Proof. split. + induction 1 as [ m x Hm | m x _ IHm ]. - apply in_split in Hm. destruct Hm as (bb & cc & Hm). exists x, nil, bb, cc; subst; auto. - destruct IHm as (y & aa & bb & cc & IHm). exists y, (x::aa), bb, cc; subst; auto. + intros (x & aa & bb & cc & Hm). subst m. apply list_has_dup_app_left. constructor 1; apply in_or_app; right. constructor 1; reflexivity. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)