proposition: Theorem gtree_mem0_restrict t r w : let t' := gtree_pair_sub (gtree_restrict t r) false in gtree_mem t' w = gtree_mem t w && gtr_mem r w.
proof: Proof. pose gm := =^~ (gtr_match0E, gtr_match1E, gtr_match2E, gtr_match3E). elim: t => /= [t0 IHt0 t1 IHt1 t2 IHt2 t3 IHt3|||||||||] in r w *; case Dr: r => [|bs ct r']; do [ by rewrite /= gtree_mem_empty ?andbF | rewrite -{bs ct r'}Dr]; try by do 2?case: ifP => /(pair gm){}gm; case: w => [|[][]] //; rewrite !gm. rewrite gtr_split_eq gtree_mem0_cons_pairs; try exact: gtree_restrict_partition. by case: w => [|s w]; rewrite // (gtr_mem_gsplit r); case: s => /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)