proposition: Lemma val_frestrict x : val (frestrict x) = f (val x).
proof: Proof. by case: x. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)