proposition: Lemma shuffle_product_cofixed :forall xs ys, shuffle_product xs ys (=) Cons ((hd xs)*(hd ys)) (pointwise_plus (shuffle_product (tl xs) ys) (shuffle_product xs (tl ys))).
proof: Proof. intros xs ys; assert (hyp_bis:=commutativity_Conv_Cons_1 Lambda_convolution coalgebra_shuffle (xs,ys)); match goal with | [ id1 : ?X1 (=) ?X2 |- _ ] => apply trans_bisimilar with X2 end; [ assumption | destruct xs as [x xs']; destruct ys as [y ys']; apply refl_bisimilar ]. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith