proposition: Lemma filter_rev {A} (f:A->bool) l : rev (filter f l) = filter f (rev l).
proof: Proof. induction l; simpl; auto. rewrite filter_app, <- IHl. simpl. destruct (f a); simpl; auto using app_nil_r. Qed.
imports: Coq(List SetoidList)