proposition: Lemma mem_insert : forall l1 l2 e a, mem a (l1 ++ l2) -> mem a (l1 ++ e :: l2).
proof: Proof. intro l1; induction l1 as [ | e1 l1]; intros l2 e a a_mem_l1l2. simpl; right; trivial. simpl in a_mem_l1l2; destruct a_mem_l1l2 as [a_eq_e1 | a_mem_l1l2]. simpl; left; trivial. simpl; right; apply IHl1; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)