proposition: Lemma switch_base f : fun_base id f (switch x y f) (pred2 x y).
proof: Proof. move=> u v ?. by rewrite [switch]lock /= -lock switchE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)