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.