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