proposition: Lemma rev_take_S_Str_nth:forall n (xs:Stream A), rev (take (S n) xs) = (Str_nth n xs) :: (rev (take n xs)).
proof: Proof. intros n; induction n; intros [x xs]; [ simpl; unfold Str_nth, Str_nth_tl, hd; reflexivity | rewrite take_S_n; unfold hd,tl; rewrite rev_cons; rewrite IHn; trivial]. Qed.
imports: List Streams Omega