proposition: Lemma hiso_id_glink (D : finType) e n f eK e' n' f' eK' : let G := @Hypermap D e n f eK in let G' := @Hypermap D e' n' f' eK' in forall (i : hiso G' G), i =1 id -> @glink G' =2 @glink G.
proof: Proof. move => G G' i iE x z. by rewrite (hiso_glink i) !iE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)