proposition: Lemma lift_path (aT : finType) (rT : eqType) (e : rel aT) (e' : rel rT) (f : aT -> rT) a p' : (forall x y, f x \in f a :: p' -> f y \in f a :: p' -> e' (f x) (f y) -> e x y) -> path e' (f a) p' -> {subset p' <= codom f} -> exists p, path e a p /\ map f p = p'.
proof: Proof. move => f_inv. elim: p' a f_inv => /= [|fb p' IH a H /andP[A B] /cons_subset[S1 S2]]; first by exists [::]. case: (codomP S1) => b E. subst. case: (IH b) => // => [x y Hx Hy|p [] *]. - by apply: H; rewrite inE ?Hx ?Hy. - exists (b::p) => /=. suff: e a b by move -> ; subst. by rewrite H ?inE ?eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)