proposition: Lemma ctree_mem_sel t e (et : colseq) : ctree_mem t (e :: et) = ctree_mem (ctree_sel t e) et.
proof: Proof. by rewrite /ctree_mem !ctree_sub_sel. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)