proposition: Lemma cpexpand_rcons (cp : cprog) s : cpexpand (rcons cp s) = cpexpand cp ++ cpexpand [:: s].
proof: Proof. by elim: cp s => [|s' cp IHcp] s //=; rewrite IHcp -catA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)