fact: Definition in_nodes (T : relType) (x y : T) (p : Path x y) : collective_pred T := [pred u | u \in nodes p].
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)