proposition: Lemma bgraph_eq_io (G : graph) (U : {set G}) (x : G) : input = output :> @bgraph G U x.
proof: Proof. by []. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)