fact: Definition open : pre_graph Lv Le := {| vset := [fset inj_v x | x in G]; eset := [fset inj_e x | x in edge G]; endpt b (e:ET) := if proj_e e is Some e' then inj_v (endpoint b e') else default; lv v := vlabel (proj_v v); le e := if proj_e e is Some e' then elabel e' else default; p_in := inj_v (input : G); p_out := inj_v (output : G) |}.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)