FDL > PVS > Graphs > graphs > Graph : type-eq-decl

Graph : TYPE = {(g:graph) | nonempty?(vert(g))}