proposition: Lemma base_skip : fun_base val f skip (pred1 (finv f z)).
proof: Proof. by move=> *; congr (_ == _); rewrite /= (canF_eq (finv_f injf)) ifN. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)