proposition: Lemma matchg_size et lb w : matchg lb et w -> size w = size et.
proof: Proof. elim: et lb w => [|e et IHet] lb [|s w] etMw //=; congr _.+1; case: s etMw. - 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)