proposition: Lemma pointwise_plus_pointwise_plus_tl :forall x xs ys, pointwise_plus_tl x xs ys (=) pointwise_plus (Cons x xs) ys.
proof: Proof. cofix. destruct xs as [x0 xs], ys as [y0 ys]. rewrite (pointwise_plus_tl_cofixed x (Cons x0 xs) (Cons y0 ys)). rewrite pointwise_plus_cofixed. constructor; trivial. apply (pointwise_plus_pointwise_plus_tl x0 xs ys). Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith