proposition: Lemma induced2_induced (G : graph2) (V :{set G}) (iV : input \in V) (oV :output \in V) : induced2 V = point (induced V) (Sub input iV) (Sub output oV).
proof: Proof. rewrite /induced2. case: {-}_ / idP; last by rewrite iV. case: {-}_ / idP; last by rewrite oV. move => p q. by rewrite (bool_irrelevance p oV) (bool_irrelevance q iV). Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)