proposition: Lemma injcp_inj cp1 cp2 : injective (@injcp cp1 cp2).
proof: Proof. elim: cp1 cp2 => [|s cp1 IHcp1] cp2 x y //; move/IHcp1{IHcp1}. by case: s => //; do 3!move/(@ecp_inj _ _ _)=> //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)