proposition: Lemma oiso2_edges_at (F G : pre_graph) (i : F ⩭2 G) z : z \in vset F -> edges_at G (i z) = [fset (efun_of i) x | x in edges_at F z].
proof: Proof. case: (efun_of_bij i) => ie_inv [I1 I2 I3] ?. rewrite /edges_at imfset_sep. apply/fsetP => e'. rewrite in_fsep. apply/andP/imfsetP => [[Ee' Ie']|[/= e2 He2 ->]]. - exists (ie_inv e'); rewrite ?I2 // inE I3 //. by rewrite -[e']I2 // -oiso2_incident // I3 in Ie'. - rewrite !inE in He2. case/andP : He2 => A B. split; first exact: im_efun_of. by rewrite -oiso2_incident. 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)