fact: Record sdecomp (T : forest) (G : sgraph) (B : T -> {set G}) := SDecomp { sbag_cover x : exists t, x \in B t; sbag_edge x y : x -- y -> exists t, (x \in B t) && (y \in B t); sbag_conn x t1 t2 : x \in B t1 -> x \in B t2 -> connect (restrict [pred t | x \in B t] sedge) t1 t2}.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)