proposition: Lemma edir_bodyE (G : pre_graph) (isG : is_graph G) (hd : (edge (pack G)) -> bool) e (He : e \in eset G) : edir_body hd e = hd (Sub e He).
proof: Proof. unlock edir_body. case: {-}_ / idP => [p|]; last by rewrite He. by rewrite (bool_irrelevance He p). Qed.
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)