proposition: Lemma ostep_of (F G : graph2) : step F G -> exists G', [/\ inhabited (ostep (open F) G') & inhabited (G' ⩭2 open G)].
proof: Proof. move/ostep_of' => [[F'] [G'] [[A B] C]]. case: (ostep_iso B (oiso2_sym A)) => H [H1 H2]. exists H. split => //. constructor. etransitivity. 2: apply: C. by symmetry. 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)