proposition: Lemma diff_mem_remove : forall l1 l2 e a, ~eqA a e -> mem a (l1 ++ e :: l2) -> mem a (l1 ++ l2).
proof: Proof. intros l1; induction l1 as [ | e1 l1]; simpl; intros l2 e a a_diff_e a_in_l1el2. destruct a_in_l1el2 as [e_eq_a | a_mem_l2]; trivial. absurd (eqA a e); trivial; symmetry; trivial. destruct a_in_l1el2 as [e1_eq_a | a_mem_l1el2]. left; trivial. right; apply (IHl1 l2 e); trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)