fact: Fixpoint config_prog (cp : cprog) := match cp with | CpR _ :: cp' => config_prog cp' | [:: CpY] => true | CpY :: cp' => config_prog cp' | CpH :: cp' => config_prog cp' | _ => false end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)