proposition: Lemma matchg_memc0 et lb w : matchg lb et w -> (Color0 \in et) = false.
proof: Proof. elim: et lb w => [|e et IHet] lb [|s w] //=; case: s. - by case: e (IHet (cbit0 e :: lb) w). - by case: e (IHet lb w). - by case: e lb (IHet (behead lb) w); do 3!case=> //. by case: e lb (IHet (behead lb) w); do 3!case=> //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)