proposition: Lemma ctree_empty_node_eq t1 t2 t3 : ctree_empty_node (CtreeNode t1 t2 t3) -> eq3_CtreeEmpty t1 t2 t3.
proof: Proof. by move: t1 t2 t3; do 3!case=> [? ? ?|?|]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)