proposition: Lemma sub_adj_injcp cp1 cp2 : {homo @injcp cp1 cp2 : x y / adj x y}.
proof: Proof. elim: cp1 cp2 => [|s cp1 IHcp] cp2 x y xAy //; case: s => *; apply: IHcp => //. - by rewrite adj_icpY. - by rewrite adj_icpH. - by rewrite adj_icpU. - exact: sub_adj_icpK. exact: sub_adj_icpA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)