proposition: Lemma ctree_cons_spec t1 t2 t3 (t := CtreeNode t1 t2 t3) : ctree_cons t1 t2 t3 = (if ctree_empty_node t then CtreeEmpty else t).
proof: Proof. by do [move: t1 t2 t3; do 3!case=> [? ? ?|?|]] in t *. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)