Support more inductive types.

Given a definition
inductive TC : TCType =
  cons : ConsType,..

the constraints are:
TCType can have arbitrary params but must return U.
ConsType must return a full TC application.
Every variable of TCType that is used anywhere in the ConsType must
occur at the correct position in every TC application in ConsType.
Every TC application in ConsType must be full and must either be
the return type, a parameter type, or the return type of a parameter type.