proposition: Lemma component_induced (G : graph2) (C : {set G}) (iC : input \in C) (oC : output \in C) : component C = point (induced C) (Sub input iC) (Sub output oC).
proof: Proof. rewrite /induced2. move: (setU11 _ _) => A. move: (setU1r _ _) => B. move: A B. rewrite (setU1_mem oC) (setU1_mem iC) => A B. by rewrite (bool_irrelevance A iC) (bool_irrelevance B oC). Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)