We need simultaneous inductive-recursive definitions! [Dyb00]
We get:
NestO :: Dnest O
NestS :: (n::N) -> (p::Dnest n) ->
Dnest (nest n p) ->
Dnest (S n)
nest :: (n::N) -> Dnest n -> N
nest O NestO = O
nest (S n) (NestS n p q) = nest (nest n p) q
No problem!
But Coq does not support this kind of definitions.