proposition: Lemma UPath_tupleK : pcancel UPath_tuple tuple_UPath.
proof: Proof. move=> [/= p Up]. case: {-}_ / boolP; last by rewrite Up. by move=> Up'; rewrite (bool_irrelevance Up' Up). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)