proposition: Theorem weakly_final_lambda_bialgebra : forall (Lambda: T_over_B_distributive), is_lambda_bialgebra Lambda (Build_TB_bialgebra w (Beta Lambda)).
proof: Proof. intros [lam_ nat_lam_] tx. assert (hyp:=commutativity_F_unfold (Build_F_coalgebra (T_ w.(states)) (fun tw=> lam_ _ (lift_T_ _ _ w.(transition) tw))) tx). symmetry. apply hyp. Qed.
imports: LambdaCoiteration