fact: Definition edir_body (G : pre_graph) (graph_G : is_graph G) (hd : edge (pack G) -> bool) (e : ET) : bool := locked (match @idP (e \in eset G) with | ReflectT p => hd (Sub e p) | ReflectF _ => false end).
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)