proposition: Lemma fib_cofixed : fib (=) Cons 0 (pointwise_plus_tl 1 fib fib).
proof: Proof. assert (hyp_bis:=commutativity_Fib_Cons_1 Lambda_fibonacci coalgebra_fibonacci tt); match goal with | [ id1 : ?X1 (=) ?X2 |- _ ] => apply trans_bisimilar with X2 end; [ assumption | apply refl_bisimilar ]. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith