proposition: Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b).
proof: Proof. induction n. reflexivity. intros [x xs] [y ys]. unfold Str_nth in *. simpl in *. apply IHn. Qed.