fact: Definition tuple_UPath (s : {n : 'I_#|G| & n.-tuple G}) : option UPath := let (_, p) := s in match boolP (upath x y p) with | AltTrue Up => Some (Sub (val p) Up) | AltFalse _ => None end.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)