proposition: Lemma icpU_node : {in [predC [:: node x0]], {morph icpU : x / node x}}.
proof: Proof. by move=> x; rewrite !inE /= => /negPf->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)