proposition: Lemma gtr_split_some bs t1 t2 t3 r0 r1 r2 r3 r : let cons_pop t t' r' := match bs with | Bstack0 => r' | Bpush0 bs' => gtr_cons bs' t r' | Bpush1 bs' => gtr_cons bs' t' r' end in gtr_split r0 r1 r2 r3 (GtrCons bs (CtreeNode t1 t2 t3) r) = gtr_split (gtr_cons (Bpush0 bs) t2 (gtr_cons (Bpush1 bs) t3 r0)) (gtr_cons bs t1 r1) (cons_pop t2 t3 r2) (cons_pop t3 t2 r3) r.
proof: Proof. by case: bs => [|bs|bs] /=; rewrite !fold_ctree_empty /gtr_cons; do 2!case: ifP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)