fact: Definition cpexpand1 (s : cpstep) : cprog := match s with | CpY => [:: CpR'; CpK; CpR 1; CpU] | CpH => [:: CpR'; CpK; CpK; CpR 1; CpU] | _ => [:: s] end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)