proposition: Lemma sskeleton_remove_io (G : graph2) (E : {set edge G}) : E \subset @edge_set _ _ G IO -> diso (sskeleton (point (remove_edges E) input output)) (sskeleton G).
proof: Proof. move=> E_subIO. exists (bij_id: bij (sskeleton (point (remove_edges E) input output)) (sskeleton G)) => //. all: rewrite /is_dhom; apply sskelP. - move=> x y. by rewrite sg_sym. - move=> e sNt. apply/orP; left. rewrite /edge_rel/=/sk_rel sNt /=. exact: adjacent_edge. - rewrite /edge_rel /= => ->. by rewrite !eqxx. - move=> x y. by rewrite sg_sym. - move=> e sNt /=. case: (boolP (e \in E)) => Ee; last first. + apply/orP; left. rewrite /edge_rel/=/sk_rel sNt /=. apply/existsP; exists (Sub e Ee). by rewrite !inE !eqxx. + move: Ee sNt => /(subsetP E_subIO). rewrite !inE /edge_rel/=. by case/andP=> /orP[]/eqP-> /orP[]/eqP->; rewrite !eqxx // eq_sym => ->. - rewrite /edge_rel/= => ->. by rewrite !eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)