proposition: Theorem eqst_ntheq : forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
proof: Proof. unfold Str_nth; simple induction n. - intros s1 s2 H; case H; trivial with datatypes. - intros m hypind. simpl. intros s1 s2 H. apply hypind. case H; trivial with datatypes. Qed.