proposition: Lemma ctree_empty_nodeP {t} : reflect (t = CtreeNode CtreeEmpty CtreeEmpty CtreeEmpty) (ctree_empty_node t).
proof: Proof. by case: t; by [right | do 3!case=> [? ? ?|?|]; constructor]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)