proposition: Lemma connect_restrictP (T : finType) (e : rel T) (A : pred T) x y (xDy : x != y) : reflect (exists p, [/\ path e x p, last x p = y, uniq (x::p) & {subset x::p <= A}]) (connect (restrict A e) x y).
proof: Proof. apply: (iffP connectUP) => [[p] [rpth_p lst_p uniq_p]|[p] [rpth_p lst_p uniq_p sub_p]]. - exists p. rewrite (sub_path _ rpth_p); first split => //; last exact: sub_restrict. apply/cons_subset; split; last exact: rpath_sub rpth_p. case: p rpth_p lst_p {uniq_p} => /= [_ /eqP E|]; by [rewrite E in xDy| case: (x \in A)]. - by exists p; case/cons_subset : sub_p => ? ?; rewrite path_rpath. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)