proposition: Lemma ctree_mem_union h tl tr et : ctree_proper h tl -> ctree_proper h tr -> ctree_mem (ctree_union tl tr) et = ctree_mem tl et || ctree_mem tr et.
proof: Proof. rewrite /ctree_mem; elim: h => [|h IHh] in tl tr et *. by case: tl; rewrite ?ctree_union_Nl //; case: tr => //; case: (et). case: tl; rewrite ?ctree_union_Nl //= => tl1 tl2 tl3 [Htlne Htl1 Htl2 Htl3]. case: tr => //= [tr1 tr2 tr3 [*]|]; last by rewrite orbF. by rewrite ctree_sub_cons; case: et => [|[] et] //=; apply: IHh. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)