proposition: Lemma emb_vertexP d1 d2 : reflect (f d1 = f d2) (cnode d1 d2).
proof: Proof. rewrite (emb_vertex emb_f). exact:eqP. 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)