proposition: Lemma filter_app : forall l m, filter f (l ++ m) = filter f l ++ filter f m.
proof: Proof. induction l; simpl; intros. refl. rewrite IHl. destruct (f a); refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)