proposition: Lemma Str_nth_map_pointwise:forall n xs (f:A->B), f (Str_nth n xs) = Str_nth n (Streams.map f xs).
proof: Proof. intros n; induction n; intros [x xs] f. unfold Str_nth, Str_nth_tl; rewrite map_spelled; trivial. rewrite map_spelled; unfold hd,tl; repeat rewrite Str_nth_S; trivial. Qed.
imports: List Streams Omega