proposition: Lemma ctree_cons_e_spec (e : color) t : let t_if_e c := if c == e then t else CtreeEmpty in ctree_cons_e e t = ctree_cons (t_if_e Color1) (t_if_e Color2) (t_if_e Color3).
proof: Proof. by case: e t => [] []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)