proposition: Proposition local_confluence (F G1 G2 : pre_graph) (isF : is_graph F) : ostep F G1 -> ostep F G2 -> exists H, osteps G1 H /\ osteps G2 H.
proof: Proof. move => S1 S2. move: (local_confluence_aux isF S1 S2) => [H1] [H2] [[S1' S2'] I]. exists H2. split => //. by rewrite-> S1', I. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)