graph_zero@{} : Graph := Build_Graph Empty (fun x y => @Empty_rec@{u} Type@{s} x) (fun x y => Empty_rec x).
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.