proposition: Lemma in_remove : forall (A : Set) (eqA : forall a1 a2 : A, {a1=a2}+{a1<>a2}) a l, match remove eqA a l with | None => ~In a l | Some l' => In a l /\ let (l1, l2) := split_list eqA l a in l' = l1 ++ l2 end.
proof: Proof. induction l as [ | a1 l]; simpl; auto; elim (eqA a a1); intro eq_a_a1; intuition. destruct (remove eqA a l) as [ rmv | ]; intuition; destruct (split_list eqA l a); subst; auto. Qed.
imports: List Arith