[[!redirects inductive recursive type]] [PDF of Peter Dybjer's 2000 paper on inductive-recursive types](http://www.cse.chalmers.se/~peterd/papers/Inductive_Recursive.pdf)