proposition: Lemma oiso2_endpoint (F G : pre_graph) (i : F ⩭2 G) (e : ET) b : e \in eset F -> endpt G b (efun_of i e) = i (endpt F (edir_of i e (+) b) e).
proof: Proof. case: i => isF isG i Ee /=. rewrite edir_bodyE efun_bodyE vfun_bodyE ?endptP // => p. by rewrite Sub_endpt -endpoint_hom /=. 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)