proposition: Lemma combine_even: forall (xs ys zs: Stream A), combine xs ys (=) zs -> xs (=) even zs.
proof: Proof. cofix. intros [x0 xs] [y0 ys] (z0 & z1 & zs) H_bisim; rewrite combine_spelled_3 in H_bisim; inversion H_bisim; constructor. inversion H0; trivial. rewrite even_spelled; apply combine_even with ys; inversion H0; assumption. Qed.
imports: List Streams Omega