proposition: Lemma not_equal_ex x y (H : ~Equal x y) : exists a, (In a x \/ In a y) /\ (In a x -> In a y -> False).
proof: Proof. revert dependent y. induction x as [|xs xs' IHxs v] using set_induction. { intro y. unfold Empty, Equal in *. setoid_rewrite (False_iff (H _)). destruct (choose y) as [v|] eqn:Hch. { setoid_rewrite_logic. apply choose_spec1 in Hch. eauto. } { apply choose_spec2 in Hch. unfold Equal, Empty in *. setoid_rewrite (False_iff (Hch _)). setoid_rewrite_logic. tauto. } } { intro y. let H := match goal with H : Add _ _ _ |- _ => H end in apply Add_Equal in H. setoid_subst xs'. setoid_rewrite add_spec. destruct (In_dec v y) as [pf|pf]; [ | exists v ]. { intro Hneq. specialize (IHxs (remove v y)). setoid_rewrite remove_spec in IHxs. destruct IHxs as [a IHxs]; [ | exists a ]. { intro Heq'; apply Hneq; clear Hneq. setoid_subst xs. rewrite add_remove by assumption. reflexivity. } { lazymatch type of IHxs with | context[E.eq ?x ?y] => assert (~E.eq x y) by (intro; rename x into x'; setoid_subst x'; firstorder auto with crelations) end. destruct_head and. destruct_head or; [ solve [ split; eauto ] | ]. destruct_head and. let H := match goal with H : _ -> _ /\ _ -> _ |- _ => H end in specialize (fun a b c => H c (conj a b)). specialize_by assumption. split; eauto; []. firstorder. } } { assert (E.eq v v) by reflexivity. eauto. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.MSets.MSetInterface Coq.MSets.MSetFacts Coq.MSets.MSetProperties Fiat.Common.Wf Fiat.Common.LogicFacts Fiat.Common.Instances Fiat.Common.NatFacts Fiat.Common.MSetExtensions Fiat.Common