fact: Definition is_weakly_final (w:F_coalgebra) := forall (S0:F_coalgebra), { F_unfold_ : S0.(states) -> w.(states) | forall s0, w.(transition) (F_unfold_ s0) = lift_F_ _ _ F_unfold_ (S0.(transition) s0)}.
imports: Bisimulation