proposition: Lemma combine_spelled_3: forall x y (xs ys:Str), combine (x|:|xs) (y|:|ys) = x|:| y |:| (combine xs ys).
proof: Proof. intros x y xs ys. rewrite combine_spelled_2. apply (@f_equal2 A Str Str (@Cons A)); trivial. apply combine_spelled_2. Defined.
imports: List Streams Omega