proposition: Lemma oiso2_remove_edges (F G : pre_graph) (i : F ⩭2 G) E E': E `<=` eset F -> E' = [fset efun_of i e | e in E] -> (F - E) ⩭2 (G - E').
proof: Proof. case: i => isF isG i /= S EE'. econstructor. have X : E' = [fset val (i.e x) | x : eset F & val x \in E]. { subst. apply/fsetP => k. apply/imfsetP/imfsetP. - case => /= x Ix ->. have Hx : x \in eset F. move: Ix. apply: (fsubsetP S). 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 - E)) : val (i.e (Sub e (fsetDl p))) \in eset G `\` E'. { rewrite inE [_ \in eset G]valP andbT X. apply: contraTN (p). case/imfsetP => /= e0. rewrite inE => A. move/val_inj. move/(@bij_injective _ _ i.e) => ?; subst. by rewrite inE A. } iso2 i (fsetD_bij (f := i.e) X) (fun k => i.d (Sub (val k) (fsetDl (valP k)))). - split. + move => [e p] b. rewrite fsetD_bijE. apply P. move => q. apply/val_inj => /=. move: (fsetDl _) => He. move: (fsetDl _) => He'. move: (endpt_proof _ _) => 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'). + move => v. rewrite /=. rewrite -(oiso2_lv (OIso2 i)) /=. 2:apply: valP. by rewrite vfun_bodyE fsvalK. + move => [e p]. rewrite fsetD_bijE => [|q]; first exact: P. case/fsetDP : (p) => p1 p2. 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. - apply: val_inj => /=. rewrite -(oiso2_input (OIso2 i)) /= vfun_bodyE ?p_inP // => q. set q' := @p_inP _ _ _ _. by rewrite (bool_irrelevance q' q). - apply: val_inj => /=. rewrite -(oiso2_output (OIso2 i)) /= vfun_bodyE ?p_outP // => q. set q' := @p_outP _ _ _ _. by rewrite (bool_irrelevance q' q). 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)