proposition: Lemma commutativity_Primitive_Corecursion_hd_tl (BT: BT_coalgebroid) (x:BT.(bs_states)) : hd (Corecursor BT x) = fst (lift_B_ _ _ (prim_corec_tupling _ (Corecursor BT)) (BT.(bs_transition) x)) /\ tl (Corecursor BT x) (=) snd (lift_B_ _ _ (prim_corec_tupling _ (Corecursor BT)) (BT.(bs_transition) x)).
proof: Proof. apply (commutativity_Primitive_Corecursion_fst_snd BT x). Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith