proposition: Lemma injcp_cat (cp1 cp2 cp3 : cprog) : pmap_eqdep (@injcp cp2 _ \o @injcp cp1 _) (@injcp (cp1 ++ cp2) cp3).
proof: Proof. elim: cp1 cp3 => [|s' cp1 IHcp] cp3; first by case cp2. rewrite cat_cons; case (injcp_cons s' (cp1 ++ cp2) cp3). by case: (IHcp (s' :: cp3)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)