proposition: Lemma flatten_filter : forall {A} (seq: list (list A)) pred, List.filter pred (flatten seq) = flatten (List.map (List.filter pred) seq).
proof: Proof. intros; induction seq; trivial. unfold flatten; simpl. induction a; trivial. simpl; destruct (pred a); simpl; rewrite IHa; trivial. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith