proposition: Lemma mem_or_app : forall l m a, mem a l \/ mem a m <-> mem a (l ++ m).
proof: Proof. intros l m a; split. induction l as [ | e l]; intros [a_mem_l | a_mem_m]. contradiction. simpl; trivial. destruct a_mem_l as [a_eq_e | a_mem_l]. simpl; left; trivial. simpl; right; apply IHl; left; trivial. simpl; right; apply IHl; right; trivial. induction l as [ | e l]; intro a_mem_lm. right; trivial. simpl in a_mem_lm; destruct a_mem_lm as [a_eq_e | a_mem_lm]. left; left; trivial. destruct (IHl a_mem_lm) as [a_mem_l | a_mem_m]. left; right; trivial. right; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)