proposition: Lemma combine_odd: forall (xs ys zs: Stream A), combine xs ys (=) zs -> ys (=) odd 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 odd_spelled; apply combine_odd with xs; inversion H0; assumption. Qed.
imports: List Streams Omega