proposition: Lemma matchg_pg et w : gram_balanced 0 false (cgram 0 false w) -> matchg [::] (ctrace et) (cgram 0 false w) = matchpg Bstack0 et w.
proof: Proof. set sb := [::]; rewrite -[Bstack0]/(stack_of_bitseq sb) /ctrace. rewrite -(add0c (sumt et)) -[Color0]/(ccons (odd 0) (sumb sb)). rewrite -(addFb (sumb sb)) -[0]/(size sb). elim: et sb false w => [|e et IHet] lb b. case=> [|s w] /=; first by do 2!case: b lb => [] [|b lb] //. move: (size lb) => d _; rewrite addc0. by case: (ccons _ _) s w => // [] [] // [] //; case: lb => [|[]]. case=> [|s w]; rewrite ?rcons_cons /=. by case: lb => [|b' [|? ?]] // _; case: e => {IHet}//; case: et => //; case b; case b'. by case: s; try (case: lb; [by [] | case=> lb /=]); case: e (IHet (cbit0 e :: lb)) => //= IHet0; do 1?[move/IHet | move/IHet0]; case: (sumt et) (odd _) b (sumb lb) => [] [] [] []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)