diff options
| author | Oliver Nash | 2019-09-03 20:38:16 +0100 |
|---|---|---|
| committer | Oliver Nash | 2019-09-03 20:38:16 +0100 |
| commit | fef9016bd3ca6544f0110bdbf8dbe6ca24120450 (patch) | |
| tree | 3c46061551808fda3534ba8e0646a00a9223f556 | |
| parent | bcf2dae1e39c6ff27c574a82c4451323a673b15f (diff) | |
Remove redundant parameter in List.concat_filter_map
| -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] *) |