fact: Definition merge_inv (G : hypermap) (x y : G) : hiso (@merge (@merge G x y) x y) G.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)