fact: Record rGraph (L : Type) := RGraph { graph_of :> graph L ; root : graph_of ; rootP x : connect (@edge _ graph_of) root x }.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)