proposition: Lemma ctree_sel_cons t1 t2 t3 e : ctree_sel (ctree_cons t1 t2 t3) e = ctree_sel (CtreeNode t1 t2 t3) e.
proof: Proof. by rewrite ctree_cons_spec; case: ctree_empty_nodeP => // ->; case: e. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)