proposition: Theorem Equiv2 : forall s1 s2 : Stream A, (forall n : nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.
proof: Proof. unfold Str_nth in |- *. cofix u. intros. apply eqst. apply (H 0). apply u. intros n. apply (H (S n)). Qed.
imports: Plus Streams