proposition: Lemma ctree_sub_0 t (et : colseq) : Color0 \in et -> ctree_sub t et = 0.
proof: Proof. by elim: et t => [|e et IHet] // [] // t1 t2 t3; case: e => //= /IHet. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)