proposition: Lemma hiso_glink (G G' : hypermap) (h : hiso G G') x y : glink x y = glink (h x) (h y).
proof: Proof. by rewrite /glink/= -hiso_edge -hiso_node -hiso_face !inj_eq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)