proposition: Lemma del_vertex_emb_proof (z : D') : g (val z) \in [set~ x].
proof: Proof. case: z => z Hz /=; rewrite !inE. apply: contraNneq Hz => E. apply: mem_closure. by rewrite inE /d -E (emb_vertex (emb_embedding g)) (emb_invK). 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)