proposition: Lemma insertE_icpY (G : hypermap) (x : G) p : insertE (map (icpY x) p) = map (icpY x) (insertE p).
proof: Proof. by elim: p => // *; do ?congr (_ :: _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)