fact: Definition induced2 (G : graph2) (V :{set G}) := match @idP (input \in V), @idP (output \in V) with | ReflectT p, ReflectT q => point (induced V) (Sub input p) (Sub output q) | _,_ => G end.
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)