fact: Fixpoint cpker (cp : cprog) : seq (cpmap cp) := match cp with | CpR _ :: cp' => cpker cp' | CpY :: cp' => map (icpY (cpmap cp')) (cpker cp') | CpH :: cp' => if cpring (cpmap cp') is [:: _, x & _] then map (icpH (cpmap cp')) (x :: cpker cp') else [::] | _ => [::] end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)