proposition: Lemma split_io_edge_lens (G : graph2) (e : edge G) : e \in edge_set IO -> lens G -> G ≃2 graph_of_term (tm_ e) ∥ point (remove_edges [set e]) input output.
proof: Proof. move => e_io lens_G. rewrite lens_io_set // inE in e_io. rewrite /tm_. case: ifP e_io => //= [e_io _|eNio e_oi]; first exact: split_io_edge. rewrite <- cnv2I. have e_io : e \in @edges _ _ (g2_cnv G) input output by []. rewrite -> (split_io_edge e_io) at 1. by rewrite -> cnv2par. 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)