path: root/test-suite/prerequisite/bind_univs.v

(* Used in output/UnivBinders.v *)

Monomorphic Definition mono@{u} := Type@{u}.

Polymorphic Definition poly@{u} := Type@{u}.

Monomorphic Universe reqU.