proposition: Theorem EqSt2_trans : forall s1 s2 s3 : Stream A, EqSt2 A s1 s2 -> EqSt2 A s2 s3 -> EqSt2 A s1 s3.
proof: Proof. cofix u. intros s1 s2 s3. intro. inversion_clear H. intro. inversion_clear H. apply eqst2. apply (u s0 s4 s6). assumption. assumption. Qed.
imports: Plus Streams