proposition: Lemma lift_pathp_on (G H : relType) (f : G -> H) a b p' : (forall x y, f x \in f a :: p' -> f y \in f a :: p' -> f x -- f y -> x -- y) -> injective f -> pathp (f a) (f b) p' -> {subset p' <= codom f} -> exists p, pathp a b p /\ map f p = p'.
proof: Proof. move => A I /andP [B /eqP C] D. case: (lift_path A B D) => p [p1 p2]; subst. exists p. split => //. apply/andP. split => //. rewrite last_map in C. by rewrite (I _ _ C). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)