fact: Definition decompU (G1 G2 : sgraph) (D1 : T1 -> {set G1}) (D2 : T2 -> {set G2}) : tjoin -> {set sjoin G1 G2} := [fun a => match a with | inl a => [set inl x | x in D1 a] | inr a => [set inr x | x in D2 a] end].
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)