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