proposition: Lemma node_injcp cp1 cp2 : cubic_prog cp1 -> {in [predC cpring (cpmap cp2)], {morph @injcp cp1 cp2 : x / node x}}.
proof: Proof. elim: cp1 cp2 => [|[n||||||] cp1 IHcp] //= cp2 cp1ok x XN'x. - by rewrite IHcp // inE /= cpring_ecpR mem_rot. - rewrite -IHcp -1?icpY_node //; first rewrite !inE mem_cpring in XN'x. by rewrite !inE; apply: contra XN'x => /pred2P[]->; rewrite -?cnode1r. rewrite inE /= cpring_ecpY -/cpmap !inE (mem_map (@icpY_inj _ _)) !orFb. by apply: contra XN'x; apply: mem_behead. - rewrite -IHcp -1?icpH_node //; first rewrite !inE mem_cpring in XN'x. rewrite !inE -/cpmap; apply: contra XN'x => /or3P. by case=> /eqP->; rewrite ?fconnect1 // cnode1r edgeK. rewrite cpring_ecpN cpring_ecpY -/cpmap; case: ifP => // _. rewrite !inE /= -map_drop -map_comp drop1 (mem_map (@icpH_inj _ _)). by apply: contra XN'x => /mem_behead/mem_behead. rewrite -IHcp -1?icpU_node ?cpring_ecpU // -/cpmap. by apply: contra XN'x; rewrite head_cpring !inE => ->. by rewrite !inE /= (mem_map (@icpU_inj _ _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)