proposition: Lemma eqdep_injcpRR' cp : pmap_eqdep [eta icpU (cpmap cp)] (@injcp (rev [:: CpR'; CpR 1; CpU]) cp).
proof: Proof. rewrite /rev /catrev /injcp -/injcp /cpmap -/cpmap. by apply pmap_eqdep_split; rewrite ecpR1_eq ecpR'_eq edgeK; case: (cpmap cp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)