proposition: Lemma injcp_expand cp1 cp2 : pmap_eqdep (@injcp (rev cp1) cp2) (@injcp (rev (cpexpand cp1)) cp2).
proof: Proof. elim: cp1 => [|s cp1 IHcp] //=; rewrite rev_cons -cats1 rev_cat. do 2!case: injcp_cat => /=; case/pmap_eqdep_sym: IHcp. move: {cp1}(rev _) => rcp. move: {cp2}(cpmap cp2) {rcp}(catrev _ cp2) (@injcp _ cp2) => A cp ic. move Dcps: (rev (cpexpand1 s)) => cps. case: s Dcps => [n||||||] //= <-{cps} //; apply: {A ic}(pmap_eqdep_comp ic); by do !apply: eqdep_injcpRK; apply: eqdep_injcpRR'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)