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