proposition: Lemma WalkupI_eq u x : val (WalkupI u x) = (if z == x then val u else x).
proof: Proof. by rewrite val_insubd if_neg eq_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)