proposition: Fact list_has_dup_app_inv l m : list_has_dup (l++m) -> list_has_dup l \/ list_has_dup m \/ exists x, In x l /\ In x m.
proof: Proof. induction l as [ | x l IHl ]; simpl; intros H; auto. apply list_hd_cons_inv in H. + destruct H as [ H | H ]. * apply in_app_or in H; destruct H as [ H | H ]. - left; constructor; auto. - do 2 right; exists x; simpl; auto. * destruct (IHl H) as [ H1 | [ H1 | (y & H1 & H2) ] ]; auto. - left; constructor 2; auto. - do 2 right; exists y; simpl; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)