diff options
| -rw-r--r-- | theories/Lists/List.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index f45317ba50..88c47b9744 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1234,11 +1234,11 @@ End Fold_Right_Recursor. destruct (f x); simpl; now rewrite IH. Qed. - Lemma concat_filter_map : forall (l : list (list A)) (f : A -> bool), + Lemma concat_filter_map : forall (l : list (list A)), concat (map filter l) = filter (concat l). Proof. induction l as [| v l IHl]; [auto|]. - simpl. rewrite (IHl f). rewrite filter_app. reflexivity. + simpl. rewrite IHl. rewrite filter_app. reflexivity. Qed. (** [find] *) |