graph : TYPE = {(g:pregraph) | FORALL (e:doubleton[T]) : edges(g)(e) IMPLIES (FORALL (x:T) : e(x) IMPLIES vert(g)(x))}