fact: Record label_preserving_graph_isomorphism_explicit `(g: @LabeledGraph V E EV EE DV DE DG) (g': @LabeledGraph V E EV EE DV DE DG) (vmap vmap': V -> V) (emap emap': E -> E): Prop := { lp_pregraph_iso: pregraph_isomorphism_explicit g g' vmap vmap' emap emap'; vlabel_iso: forall v, vvalid g v -> vlabel g v = vlabel g' (vmap v); elabel_iso: forall e, evalid g e -> elabel g e = elabel g' (emap e); }.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext