proposition: Lemma matchg_cgram cw et : matchg [::] (ctrace et) cw -> cw = cgram 0 false (take (size cw).-1 cw).
proof: Proof. move=> etMcw; have [_] := matchg_balanced etMcw; rewrite sumt_ctrace /=. case: cw etMcw 0 false => [|s w _] /=; first by case et. elim: w s => [|s' w IHw] s d b0; first by case: s b0 d; do 3!case=> //. by case: s => //= etMw; congr (_ :: _); apply: IHw; case: d etMw; case b0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)