proposition: Lemma homo_path_in x s : {in P &, {homo f : x y / e x y >-> e' x y}} -> all P (x :: s) -> path e x s -> path e' (f x) (map f s).
proof: Proof. by move=> f_mono; rewrite path_map; apply: sub_in_path. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)