proposition: Lemma even_oddth:forall xs n, Str_nth n (even xs) = Str_nth (2*n) xs.
proof: Proof. intros xs n. generalize xs. clear xs. induction n. intros xs. rewrite even_spelled_2. unfold Str_nth. reflexivity. intros xs. unfold Str_nth. replace (2 * (S n)) with (S (2*n+1)); try omega. simpl. replace (n + (n + 0) + 1) with (S (2*n)); try omega. simpl. replace (n + (n + 0)) with (2*n); try omega. apply (IHn (tl (tl xs))). Defined.
imports: List Streams Omega