proposition: Lemma eqdep_injcpRK cp dcp (G : pointed_map) (h : cpmap cp -> G) : pmap_eqdep [eta h] (@injcp (rev (CpR' :: dcp)) cp) -> pmap_eqdep (icpN G \o h) (@injcp (rev [:: CpR', CpK & dcp]) cp).
proof: Proof. rewrite -[_ \o _]/(_ \o [eta h]) => /pmap_eqdep_sym[] {G h}. rewrite !rev_cons -!cats1 -catA cat1s; do 2!case: injcp_cat. move: {cp}(cpmap cp) {dcp}(catrev _ cp) (@injcp _ cp) => A cp'. rewrite /catrev /injcp /cpmap -/cpmap; case/cpmap: cp' => G' x f. by apply pmap_eqdep_split; rewrite /icpK /ecpK !ecpR1_eq !ecpR'_eq edgeK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)