proposition: Fact perm_list_has_dup l m : l ~p m -> list_has_dup l -> list_has_dup m.
proof: Proof. induction 1 as [ | x l m H1 IH1 | x y l | ]; auto; intros H; apply list_hd_cons_inv in H. + destruct H as [ H | H ]. * apply Permutation_in with (1 := H1) in H. apply in_list_hd0; auto. * apply in_list_hd1; auto. + destruct H as [ [ H | H ] | H ]; subst. * apply in_list_hd0; left; auto. * apply in_list_hd1, in_list_hd0; auto. * apply list_hd_cons_inv in H. destruct H as [ H | H ]. - apply in_list_hd0; right; auto. - do 2 apply in_list_hd1; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)