proposition: Lemma homo_path x s : {homo f : x y / e x y >-> e' x y} -> path e x s -> path e' (f x) (map f s).
proof: Proof. by move=> f_homo; rewrite path_map; apply: sub_path. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)