diff options
| -rw-r--r-- | theories/Lists/Streams.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 909c6b49f9..472265f3e3 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -146,6 +146,15 @@ Inductive Exists ( x: Stream ) : Prop := CoInductive ForAll (x: Stream) : Prop := HereAndFurther : P x -> ForAll (tl x) -> ForAll x. +Lemma ForAll_Str_nth_tl : forall m x, ForAll x -> ForAll (Str_nth_tl m x). +Proof. +induction m. + tauto. +intros x [_ H]. +simpl. +apply IHm. +assumption. +Qed. Section Co_Induction_ForAll. Variable Inv : Stream -> Prop. |