proposition: Lemma nats_cofixed : nats (=) Cons 0 (map_ (fun x=>x+1) nats).
proof: Proof. assert (hyp_bis:=commutativity_map_S_Cons_1 Lambda_map_S coalgebra_map_S tt); match goal with | [ id1 : ?X1 (=) ?X2 |- _ ] => apply trans_bisimilar with X2 end; [ assumption | apply refl_bisimilar ]. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith