proposition: Lemma merge_inv_eqm (G : hypermap) (x y : G) : @merge (@merge G x y) x y =m G.
proof: Proof. case: G x y => D e n f /= eK x y; apply: EqHypermapEN => //=. exact: switchK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)