Inductive test : $(let U := type of Type in exact U)$ := t.