proposition: Lemma commutativity_Primitive_Corecursion_Cons (BT: BT_coalgebroid) (x:BT.(bs_states)) : Corecursor BT x (=) Cons (fst (lift_B_ _ _ (prim_corec_tupling _ (Corecursor BT)) (BT.(bs_transition) x))) (snd (lift_B_ _ _ (prim_corec_tupling _ (Corecursor BT)) (BT.(bs_transition) x))).
proof: Proof. rewrite (hd_tl_id (Corecursor BT x)). destruct (commutativity_Primitive_Corecursion_hd_tl BT x) as [hyp_hd hyp_tl]. constructor. rewrite hyp_hd; reflexivity. unfold tl at 1. match goal with | [ id1 : ?X1 (=) ?X2 |- _ ] => apply trans_bisimilar with X2; trivial end. apply refl_bisimilar. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith