Renamed J to rec, make U's type equal to U.

Making U of type U seems to be a bit dangerous.  However,
I believe that it is sound for the following reasons: You
could think of U as having an index, U_i is of type U_{i+1}.
Now our type constructors containing U are really polymorphic
functions:
TC : A:U_k -> B:U_l -> U_{max(k,l)}  (for every k,l)
similarly the corresponding constructors:
TC.cons : A:U_k -> B:U_l -> ... -> TC A B
The recursion operator has the type
TC.rec : A:U_k -> B:U_l -> C:(.... -> U_m) -> ..... t : TC A B -> C t
(no computation with indices needed)
Also a user defined polymorphic operator automatically has a sane type,
e.g.
\A:U \B:U TC A b  has type  A:U_k -> B:U_l -> TC A B  (for all k l)
   (whereas TC A B  has type  U_{max(k,l)})
Since all functions taking a parameter of type U are defined for every
possible index of U, we never have to check the index of U.  Therefore,
we can even omit the index and say that U has type U.