proposition: Lemma oiso2_pIO_vfun (F G : pre_graph) (isF : is_graph F) (isG : is_graph G) (i : pack F ≃2 pack G) z (Vz : z \in vset F) : z \in pIO F = (val (i (Sub z Vz)) \in pIO G).
proof: Proof. by rewrite (oiso2_pIO (OIso2 i)) //= vfun_bodyE. 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)