proposition: Theorem Equiv1 : forall s1 s2 : Stream A, EqSt s1 s2 -> forall n : nat, Str_nth n s1 = Str_nth n s2.
proof: Proof. unfold Str_nth in |- *. fix u 4. intros s1 s2 H n. case H. intros. case n. assumption. intros. simpl in |- *. apply u. assumption. Qed.
imports: Plus Streams