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