fact: Definition Lam_coiterator (Lambda:T_over_B_distributive) (BS: BT_coalgebroid) : BS.(bs_states) -> w.(states) := match BS with | Build_BT_coalgebroid X X_tr => let i0 := T_star_coproject_ X 0 in let T_star_phi := lift_T_star_ _ _ X_tr in let lambda_star_SX := lambda_star Lambda (T_ X) in let B_Chi_X := lift_B_ _ _ (Chi X) in let h := F_unfold (Build_F_coalgebra (T_star_ X) (fun x=> B_Chi_X (lambda_star_SX (T_star_phi x)))) in fun x => h (i0 x) end.
imports: WeaklyFinalCoalgebra