proposition: Lemma gtr_match0E r : gtr_match0 r = gtr_mem r [:: Gpush].
proof: Proof. by elim: r => //= bs [] //= t1 t2 t3 r <-; case: t2 => //; case: t3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)