fact: Definition ccons b1 b0 := match b1, b0 with | false, false => Color0 | false, true => Color1 | true, false => Color2 | true, true => Color3 end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)