Definition has_nodeset (G : precgraph) : UU := isaset (node G).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.