Definition onnode {G H : precgraph} : cgraph_mor G H → node G → node H := pr1.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.