Definition make_graph (G : pregraph) (h : has_vertexset G) (k : has_edgesets G) : graph := G,, make_dirprod h k.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.