fact: Fixpoint take_conat (bound:nat) (n:conat) {struct bound}: unit + nat := match bound, n with | O, co_O => inr unit O | O, co_S n' => inl nat tt | S b', co_O => inr unit O | S b', co_S n' => match take_conat b' n' with | inl u => inl nat u | inr n'' => inr unit (S n'') end end.
imports: WeaklyFinalCoalgebra