fact: Definition Beta (Lambda:T_over_B_distributive) : T_ w.(states) -> w.(states):= match Lambda with | Build_T_over_B_distributive lam_ _=> F_unfold (Build_F_coalgebra _ (fun s_bx=> lam_ _ (lift_T_ _ _ (transition w) s_bx))) end.
imports: WeaklyFinalCoalgebra