proposition: Lemma injcp_cons s (cp1 cp2 : cprog) : pmap_eqdep (fun x => @injcp cp1 (s :: cp2) (injcp [:: s] x)) (@injcp (s :: cp1) cp2).
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)