proposition: Lemma connectUP (T : finType) (e : rel T) (x y : T) : reflect (exists p, [/\ path e x p, last x p = y & uniq (x::p)]) (connect e x y).
proof: Proof. apply: (iffP connectP) => [[p p1 p2]|]; last by firstorder. exists (shorten x p). by case/shortenP : p1 p2 => p' ? ? _ /esym ?. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)