proposition: Lemma oiso2_pIO (F G : pre_graph) (i : F ⩭2 G) z : z \in vset F -> (z \in pIO F) = (i z \in pIO G).
proof: Proof. Proof with eauto with typeclass_instances. move => Vz. apply/idP/idP. - rewrite !inE. case/orP => /eqP ->; by rewrite ?oiso2_input ?oiso2_output eqxx. - rewrite !inE. case/orP => /eqP. + rewrite -(oiso2_input i). move/vfun_of_inj => -> //; first by rewrite eqxx. eapply p_inP... + rewrite -(oiso2_output i). move/vfun_of_inj => -> //; first by rewrite eqxx. eapply p_outP... 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)