proposition: Lemma filter_incl : forall l, filter f l [= l.
proof: Proof. induction l; simpl; intros. refl. case (f a); rewrite IHl. refl. apply incl_tl. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)