proposition: Lemma oiso_of (G H: graph2): G ≃2 H -> open G ⩭2 open H.
proof: Proof. intro. apply (@OIso2 _ _ (open_is_graph G) (open_is_graph H)). etransitivity. symmetry. apply openK. etransitivity. eassumption. apply openK. 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)