proposition: Lemma gtr_mem_cons bs t r w : gtr_mem (gtr_cons bs t r) w = has_match bs (ctree_mem t) w || gtr_mem r w.
proof: Proof. rewrite /gtr_cons; case: ifP => // /ctree_empty_eq-> /=; rewrite orb_idl //. by case/has_matchP; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)