The proof rules will ensure that the following two assertions hold.
rec(x,y.A;b) typeThat is, rec(x,y.A;b) is a type exactly when there is a type B and universe level k such that b is in B and for all x which, when instantiated with a value from B, yield a type at universe k, and y of type b, A (with x and y potentially free) is a type. Also, t is of type rec(x,y.A;b) exactly when rec(x,y.A;b) is a type and t is a member of the ``unwinding'' of the recursive type.
& x:(B->Uk)->y:B->A type
rec(x,y.A;b)
rec(x,y.A;b) type
&\y .rec(x,y.A;y)
