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