proposition: Theorem trans_EqSt : forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.
proof: Proof. coinduction Eq_trans. transitivity (hd s2). case H; intros; assumption. case H0; intros; assumption. apply (Eq_trans (tl s1) (tl s2) (tl s3)). case H; trivial with datatypes. case H0; trivial with datatypes. Qed.