proposition: Lemma lambda_convolution_natural: forall (X Y : Set) (f : X -> Y) (sbx : T_ (B_ X)), lambda_convolution Y (lift_T_ (B_ X) (B_ Y) (lift_B_ X Y f) sbx) = lift_B_ (T_ X) (T_ Y) (lift_T_ X Y f) (lambda_convolution X sbx).
proof: Proof. intros X Y f [[b0 x0] [b1 x1]]; trivial. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith