proposition: Lemma openK (G : graph2) : G ≃2 pack (open G).
proof: Proof. iso2 (imfset_bij (@inj_v_inj G)) (imfset_bij (@inj_e_inj (edge G))) (fun => false) => /=. 2-3: exact: val_inj. split. - move => e b. apply: val_inj => /=;by rewrite !inj_eK. - move => v /=. by rewrite inj_vK. - move => e /=. by rewrite inj_eK. Defined.
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)