What about nested recursion

• Consider the following:
  nest :: N -> N nest O = O nest (S n) = nest (nest n)
• The mechanically constructed domain predicate becomes
  Dnest :: N -> Prop NestO :: Dnest O NestS :: (n::N) -> Dnest n -> Dnest (nest n) -> Dnest (S n)
• The domain predicate needs to refer to the function! The above definition is not correct!