fact: Definition frestrict (x : sig P) : sig P := let: exist vx Px := x in Sub (f vx) (hom_f Px).
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)