proposition: Lemma pointwise_plus_cofixed :forall xs ys, pointwise_plus xs ys = Cons ((hd xs)+(hd ys)) (pointwise_plus (tl xs) (tl ys)).
proof: Proof. intros xs ys. unfold pointwise_plus, Beta, Lambda_convolution, F_unfold. simpl; rewrite Str_unfold_unfolded. reflexivity. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith