proposition: Lemma gtr_mem_gsplit r s w : gtr_mem r (s :: w) = gtr_mem (gsplit r s) w.
proof: Proof. rewrite /gsplit; move Drn: GtrNil => rn; rewrite -[lhs in lhs = _]orFb. have <-: gtr_mem (@gram_symbol_rec (fun _ => _) rn rn rn rn s) w = false. by rewrite -Drn; case: s. elim: r rn {2 4}rn {3 6}rn {4 8}rn {Drn}; first by move=> *; rewrite /= orbF. move=> bs [t1 t2 t3|lf|] r IHr r0 r1 r2 r3; rewrite ?gtr_split_some -?{}IHr; try by rewrite [s :: w]lock /= -lock; case: has_matchP => [[[]] | ]. case: s; rewrite /= ?gtr_mem_cons orbA {-2 3}[orb]lock orbC -?orbA -!lock //; by case: bs => *; rewrite ?gtr_mem_cons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)