proposition: Lemma sub_cface_icpA : subrel (cface : rel G) (cface : rel ecpA).
proof: Proof. apply: connect_sub => x _ /eqP<-; rewrite (@cface1 ecpA) /= {2}/ecpA_face. have:= ecpA_merge; rewrite cfaceC edgeK => nx0Ffex0. by case: ifP => // _; do 2!case: eqP => [-> //|_]; rewrite (@cfaceC ecpA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)