proposition: Lemma map__cofixed :forall g xs, map_ g xs = Cons (g (hd xs)) (map_ g (tl xs)).
proof: Proof. intros g xs. unfold map_, Beta, Lambda_map_S, F_unfold. simpl; rewrite Str_unfold_unfolded. reflexivity. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith