proposition: Lemma ctree_mem_disjoint tl tr et : ctree_disjoint tl tr -> ctree_mem tr et -> ctree_mem tl et = false.
proof: Proof. move=> tl'tr tr_et; apply: contraTF tl'tr => tl_et. by apply/ctree_mem_disjoint_spec; exists et; apply/andP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)