proposition: Lemma odd_even_tl:forall s, odd s (=) (even (tl s)).
proof: Proof. cofix. intros [x [y xs]]. rewrite odd_spelled. simpl. rewrite even_spelled_2. constructor. reflexivity. simpl. apply odd_even_tl. Defined.
imports: List Streams Omega