proposition: Lemma ctree_sub_sel t e (et : colseq) : ctree_sub t (e :: et) = ctree_sub (ctree_sel t e) et.
proof: Proof. by case: t e => [t1 t2 t3|lf|] // []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)