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