proposition: Lemma ctr_split_some bs t0 t1 t2 t3 r1 r2 r3 r : let cons_pop t t' r' := match bs with | Bstack0 => r' | Bpush0 bs' => ctr_cons bs' t r' | Bpush1 bs' => ctr_cons bs' t' r' end in ctr_split r1 r2 r3 (CtrCons bs (GtreeNode t0 t1 t2 t3) r) = ctr_split (ctr_cons bs t1 r1) (ctr_cons (Bpush0 bs) t0 (cons_pop t2 t3 r2)) (ctr_cons (Bpush1 bs) t0 (cons_pop t3 t2 r3)) r.
proof: Proof. by case: bs => [|bs|bs] /=; rewrite !fold_gtree_empty /ctr_cons; case: ifP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)