proposition: Lemma commutativity_Fib_hd_tl (Lambda:T_over_B_distributive) (BS: BT_coalgebroid) (x:BS.(bs_states)) : hd (Lam_coiterator Lambda BS x) = fst (lift_B_ _ _ (Beta Lambda) (lift_B_ _ _ (lift_T_ _ _ (Lam_coiterator Lambda BS)) (bs_transition BS x))) /\ tl (Lam_coiterator Lambda BS x) (=) snd( lift_B_ _ _ (Beta Lambda) (lift_B_ _ _ (lift_T_ _ _ (Lam_coiterator Lambda BS)) (bs_transition BS x))).
proof: Proof. apply (commutativity_Fib_fst_snd Lambda BS x). Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith