fact: Definition irred_of (p0 : UPath x y) : IPath := let (p,Up) := p0 in (Sub (Build_Path (upathW Up)) (upath_irred Up)).
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)