proposition: Lemma openKE (G : graph2) (x : G) : openK G x = pack_v (inj_v x) :> pack (open G).
proof: Proof. rewrite /pack_v /=. case: {-}_ /idP => [p|np]. - by apply: val_inj => /=. - by rewrite in_imfsetT in np. 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)