proposition: Lemma pointwise_plus_pointwise_plus_tl_2 :forall x xs ys, pointwise_plus_tl x xs ys (=) pointwise_plus (Cons x xs) ys.
proof: Proof. intros x xs ys. destruct (maximal_bisimulation_is_maximal w w) as [_ hyp]. set (R':=fun alpha beta => exists x, exists xs, exists ys, alpha = pointwise_plus_tl x xs ys /\ beta = pointwise_plus (Cons x xs) ys). apply (hyp R'). assert (R'_bis:is_F_bisimulation_strong w w R') ;[|exists R'_bis; trivial]. clear; exists (gamma_pointwise_plus_pointwise_plus_tl). intros [[xs ys] hyp]; split; simpl; trivial; f_equal. destruct hyp as (x0 & xs0 & ys0 & hyp1 & hyp2). simpl in hyp1,hyp2; rewrite hyp1, hyp2, pointwise_plus_cofixed, pointwise_plus_tl_cofixed; trivial. exists x; exists xs;exists ys; split; trivial. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith