proposition: Lemma emb_path x y (p : Path x y) : exists (q : seq D), [/\ path clink (emb_inv x) q, f (last (emb_inv x) q) = y & {in q, forall z, f z \in p}].
proof: Proof. have plainD := emb_plain emb_f. elim/Path_ind : p => {x} => [|x z p xz [r [R1 R2 R3]]]. by exists nil; split => //=; rewrite ?emb_invK. have [q [Q1 Q2 Q3]] := edge_clink xz. exists (q++r); rewrite cat_path last_cat !Q1 Q2 R1 R2; split => // v. rewrite !inE mem_cat => /orP [Hv|/R3->//]. by rewrite mem_edgep -in_set2 Q3 // imset_f. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)