proposition: Lemma ecp_eqP : Equality.axiom ecp_eq.
proof: Proof. case=> [||x] [||y]; by [constructor | apply: (iffP eqP) => [->|[]]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)