proposition: Lemma ctree_mem_disjoint_spec tl tr : reflect (exists et, ctree_mem tl et && ctree_mem tr et) (~~ ctree_disjoint tl tr).
proof: Proof. have Ineg := @negbT (ctree_disjoint _ _). elim: tl tr => [tl1 IH1 tl2 IH2 tl3 IH3 | lfl IHl|] [tr1 tr2 tr3|lfr|]; try by [right=> [[[|? ?]]] //=; rewrite ?andbF | left; exists nil]. rewrite /= -if_neg; case: IH1 => [tlr_et | tl'r1]. by left; have [et] := tlr_et; exists (Color1 :: et). rewrite /= -if_neg; case: IH2 => [tlr_et | tl'r2]. by left; have [et] := tlr_et; exists (Color2 :: et). case: IH3 => [tlr_et | tl'r3]; [left | right]. by have [et] := tlr_et; exists (Color3 :: et). by case=> -[|[] et] //= ?; [case: tl'r1 | case: tl'r2 | case: tl'r3]; exists et. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)