proposition: Lemma concat_filter_map : forall (l : list (list A)), concat (map filter l) = filter (concat l).
proof: Proof. intro l; induction l as [| v l IHl]; [auto|]. simpl. rewrite IHl. rewrite filter_app. reflexivity. Qed.
imports: PeanoNat