proposition: Lemma ctree_cons_pairs_spec t1 t1' t2 t2' t3 t3' : ctree_cons_pairs (CtreePair t1 t1') (CtreePair t2 t2') (CtreePair t3 t3') = CtreePair (ctree_cons t1 t2 t3) (ctree_cons t1' t2' t3').
proof: Proof. by rewrite 2!ctree_cons_spec /=; do 2!case: ifP => _. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)