fact: Definition Path_of_path (G : relType) (x : G) (p : seq G) (pth_p : path (--) x p) := Build_Path (Path_of_proof pth_p).
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)