proposition: Lemma removeA_filter : forall x l, removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
proof: Proof. intros x l; induction l as [|a l IHl]; simpl; auto. destruct (eqA_dec x a); auto. rewrite IHl; auto. Qed.
imports: List Sorted Setoid Basics Morphisms