proposition: Lemma cpmap_simple cp : config_prog cp -> simple (cpring (cpmap cp) ++ cpker cp).
proof: Proof. elim: cp => [|s cp IHcp] //=; case: s => // [n||] cp_ok. - by rewrite cpring_ecpR /rot -catA simple_catCA catA cat_take_drop IHcp. - rewrite cpring_ecpY cat_cons simple_cons. rewrite (closed_connect (fbandF _) (cface_node_ecpY _)). rewrite -simple_cons -cat1s catA -cat_rcons -cats1 -!catA simple_catCA. rewrite /= -map_cat -map_cons -cat_cons -head_cpring simple_cons. rewrite unfold_in (eq_has (@cface_ecpY _ _)) has_map has_pred0 /=. rewrite (simple_map (cface_icpY _)); case: cp IHcp cp_ok => // _ _. by rewrite cpring0 simple_cons unfold_in /= fconnect_id. set G := cpmap cp; have properG := cpmap_proper (config_prog_cubic cp_ok). rewrite cpring_ecpH // {2}head_proper_cpring // -/G cat_cons simple_cons. rewrite (closed_connect (fbandF _) (cface_node_ecpH _)) // -simple_cons -cat1s. rewrite catA -!cat_rcons -!cats1 -!catA simple_catCA 2!catA simple_catCA. rewrite -catA simple_catCA -map_cat -!catA !cat1s -!map_cons -!cat_cons. rewrite -head_proper_cpring // simple_cons (simple_map (cface_icpH G)). by rewrite unfold_in (eq_has (cface_ecpH _)) // has_map has_pred0 IHcp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)