proposition: Lemma pmap_eqdep_comp A B f G G' h h' : @pmap_eqdep B G [eta h] G' [eta h'] -> @pmap_eqdep A G (h \o f) G' (h' \o f).
proof: Proof. by rewrite -[h' \o f]/([eta h'] \o f); case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)