proposition: Lemma mem_app_eq : forall l1 l2 x, mem x (l1 ++ l2) = (mem x l1 \/ mem x l2).
proof: Proof. Proof using. intros. extens. induction l1; rew_list. { split. { auto. } { introv [H|?]. inverts H. auto. } } { iff M. { inverts~ M. rewrite IHl1 in H0. destruct* H0. } { destruct M. inverts~ H. constructors. rewrite~ IHl1. constructors. rewrite~ IHl1. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)