proposition: Lemma ctree_mem_cons t1 t2 t3 et : ctree_mem (ctree_cons t1 t2 t3) et = ctree_mem (CtreeNode t1 t2 t3) et.
proof: Proof. by rewrite /ctree_mem ctree_sub_cons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)