Inductive PBox : Prop :=
| wrap : forall P:Prop, P -> PBox.

Inductive TBox : Type :=
| wrap_t : forall T:Type, T -> TBox.

Check (wrap PBox).

Fail Check (wrap_t TBox).