diff options
Diffstat (limited to 'theories/Lists/Streams.v')
| -rwxr-xr-x | theories/Lists/Streams.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index f5f15d889..d63fcac2b 100755 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -43,7 +43,7 @@ Qed. Lemma tl_nth_tl : (n:nat)(s:Stream)(tl (Str_nth_tl n s))=(Str_nth_tl n (tl s)). Proof. Induction n; Simpl; Auto. -Save. +Qed. Hints Resolve tl_nth_tl : datatypes v62. Lemma Str_nth_tl_plus @@ -51,12 +51,12 @@ Lemma Str_nth_tl_plus Induction n; Simpl; Intros; Auto with datatypes. Rewrite <- H. Rewrite tl_nth_tl; Trivial with datatypes. -Save. +Qed. Lemma Str_nth_plus : (n,m:nat)(s:Stream)(Str_nth n (Str_nth_tl m s))=(Str_nth (plus n m) s). Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes. -Save. +Qed. (** Extensional Equality between two streams *) |