diff options
| -rw-r--r-- | theories/Lists/Streams.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 310c651e8..8a01b8fb1 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -196,7 +196,7 @@ Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P (map s)) S <-> ForAll P (map S). Proof. intros P S. -split; generalize S; clear S; cofix; intros S; constructor; +split; generalize S; clear S; cofix ForAll_map; intros S; constructor; destruct H as [H0 H]; firstorder. Qed. |