fact: Fixpoint injcp (cp1 cp2 : cprog) (x : cpmap cp2) : cpmap (catrev cp1 cp2) := match cp1 with | [::] => x | s :: cp1' => let x' := match s return cpmap (s :: cp2) with | CpY => icpY (cpmap cp2) x | CpH => icpH (cpmap cp2) x | CpU => icpU (cpmap cp2) x | CpK => icpK (cpmap cp2) x | _ => x end in injcp cp1' x' end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)