proposition: Theorem gtree_restrict_partition t r : gtree_pair_partition t (gtree_restrict t r).
proof: Proof. elim: t r => [t0 IHt0 t1 IHt1 t2 IHt2 t3 IHt3|||||||||] r /=; case Dr: r => [|bs ct r']; do [exact: gtpr | rewrite -{r' ct bs}Dr]; by [ case: ifP => _; [apply: gtpl | apply: gtpr] | do 2![case: ifP] => _ _ [|[] []] | rewrite gtr_split_eq; apply: gtree_cons_pairs_partition]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)