(* -*- coq-prog-args: ("-type-in-type"); -*- *)

Definition some_prop : Prop := Type.