fact: Definition lambda_corecursion (X:Set) (tbx:T_ (B_ X)) : B_ (T_ X) := match tbx with | inl bx => lift_B_ X (T_ X) (il X) bx | inr w0 => lift_B_ w.(states) (T_ X) (ir X) (w.(transition) w0) end.
imports: WeaklyFinalCoalgebra