From 2ed747a81ed14d91112b9b3360c6e5ab4ff897eb Mon Sep 17 00:00:00 2001
From: roconnor
Date: Wed, 11 Jul 2007 15:25:03 +0000
Subject: Added ForAll_Str_nth_tl

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9967 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/Streams.v | 9 +++++++++
 1 file changed, 9 insertions(+)

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.
-- 
cgit v1.2.3