proposition: Lemma oiso2_remove_vertex (F G : pre_graph) (z : VT) (j : F ⩭2 G) : z \in vset F -> z \notin pIO F -> F \ z ⩭2 G \ j z.
proof: Proof. move: j => [isF isG i] Vz IOz /=. unshelve econstructor. { apply remove_vertex_graph => //; constructor. rewrite (oiso2_pIO (OIso2 i)) // in IOz. } have E1 : [fset vfun_body i z] = [fset val (i x) | x : vset F & val x \in [fset z]]. { apply/fsetP => k. rewrite inE vfun_bodyE. apply/eqP/imfsetP => /= [->|[x] /= ]. - exists (Sub z Vz) => //. by rewrite !inE. - rewrite !inE => /eqP X ->. move: Vz. rewrite -X => Vz. by rewrite fsvalK. } have E2 : edges_at G (vfun_body i z) = [fset val (i.e x) | x : eset F & val x \in edges_at F z]. { rewrite (@oiso2_edges_at _ _ (OIso2 i)) //=. apply/fsetP => k. apply/imfsetP/imfsetP. - case => /= x Ix ->. have Hx : x \in eset F. move: Ix. rewrite edges_atE. by case: (_ \in _). exists (Sub x Hx) => //. by rewrite efun_bodyE. - case => /= x. rewrite inE => Hx ->. exists (fsval x) => //. by rewrite efun_bodyE fsvalK. } - have P e (p : e \in eset (F \ z)) : val (i.e (Sub e (fsetDl p))) \in eset G `\` edges_at G (vfun_body i z). { rewrite inE [_ \in eset G]valP andbT E2. apply: contraTN (p). case/imfsetP => /= e0. rewrite inE => A. move/val_inj. move/(@bij_injective _ _ i.e) => ?; subst. by rewrite inE A. } have Q v (p : v \in vset (F \ z)) : val (i (Sub v (fsetDl p))) \in vset G `\ vfun_body i z. { rewrite inE [_ \in vset G]valP andbT E1. apply: contraTN (p). case/imfsetP => /= v0. rewrite inE => A. move/val_inj. move/(@bij_injective _ _ i) => ?; subst. by rewrite inE A. } iso2 (fsetD_bij (f := i) E1) (fsetD_bij (f := i.e) E2) (fun k => i.d (Sub (val k) (fsetDl (valP k)))). + split. * case => e p b. rewrite fsetD_bijE. apply: P. move => q. rewrite /=. apply/val_inj => /=. move: (fsetDl _) => He. move: (fsetDl _) => He'. move: (fsetDl _) => Hv. rewrite [fsval _](_ : _ = (efun_of (OIso2 i) e)) ?(@oiso2_endpoint _ _ (OIso2 i)) //=. rewrite vfun_bodyE; first exact: endptP. rewrite edir_bodyE => Hv'. by rewrite (bool_irrelevance Hv Hv'). by rewrite efun_bodyE (bool_irrelevance He He'). * case => v p. case/fsetD1P : (p) => p1 p2. rewrite fsetD_bijE. apply: Q. move => q. rewrite ![vlabel _]/=. rewrite -(oiso2_lv (OIso2 i)) //= vfun_bodyE. by rewrite (bool_irrelevance (fsetDl p) p2). * case => e p. case/fsetDP : (p) => p1 p2. rewrite fsetD_bijE. apply: P. move => q. rewrite ![elabel _]/=. rewrite [i.d _]/=. move: (oiso2_le (OIso2 i) p1) => H. apply: eqvb_transR H => //=. rewrite edir_bodyE efun_bodyE. rewrite (bool_irrelevance (fsetDl p) p1). rewrite (bool_irrelevance (fsetDl (valP [` p])) p1) addbb. done. + rewrite fsetD_bijE. apply: Q. move => q. apply/val_inj => /=. rewrite -(oiso2_input (OIso2 i)) /= vfun_bodyE. apply: p_inP. move => r. set X := fsetDl _. by rewrite (bool_irrelevance X r). + rewrite fsetD_bijE. apply: Q. move => q. apply/val_inj => /=. rewrite -(oiso2_output (OIso2 i)) /= vfun_bodyE. apply: p_outP. move => r. set X := fsetDl _. by rewrite (bool_irrelevance X r). 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)