proposition: Lemma fold_ctree_empty A (ve vne : A) t : (if t is CtreeEmpty then ve else vne) = (if ctree_empty t then ve else vne).
proof: Proof. by case : t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)