fact: Fixpoint remove (A : Set) (eqA : forall a1 a2 : A, {a1=a2}+{a1<>a2}) (a : A) (l : list A) {struct l} : (option (list A)) := match l with | nil => None | h :: tl => if eqA a h then Some tl else match remove eqA a tl with | Some rmv => Some (h :: rmv) | None => None end end.
imports: List Arith