proposition: Lemma split_io_loop (G : graph2) (e : edge G) : e \in edge_set IO -> input == output :> G -> G ≃2 graph_of_term (tm_ e) ∥ point (remove_edges [set e]) input output.
proof: Proof. move => e_io /eqP Eio. rewrite inE -Eio setUid !inE in e_io. rewrite /tm_ inE -Eio e_io {2}Eio /=. apply: split_io_edge. by rewrite inE -Eio. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(bij set_tac digraph sgraph minor checkpoint) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(skeleton bounded equiv extraction_def)