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