proposition: Lemma mem_last_eq_cases : forall x y l, mem x (l&y) = ((x <> y /\ mem x l) \/ (x = y)).
proof: Proof. Proof using. intros. extens. induction l; rew_list. { tests: (x = y). { autos*. } { iff M. { inverts~ M. } { destruct M as [(?&H)|]. { inverts~ H. } { subst*. } } } } { tests: (x = y). { autos*. } { iff M. { inverts M as M'; auto. rewrite IHl in M'. destruct* M'. } { destruct M as [(?&H)|]. { inverts~ H. constructors. rewrite* IHl. } { constructors. rewrite~ IHl. } } } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)