Definition precgraph_of_cgraph : cgraph → precgraph := pr1.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.