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