fact: Definition del_vertex_emb (z : D') : G' := Sub (g (val z)) (del_vertex_emb_proof z).
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)