Fib.hss

flatten-module
binding-of 'fib
{
  ww-split-unsafe [| wrap Nat |] [| unwrap Nat |]
  {rhs-of 'work
    unfold 'unwrap
    any-call (unfold 'f)
    { consider lam ; alpha-lam 'm }
  }
  simplify
  any-call (unfold 'wrap)
}