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