proposition: Lemma ctree_of_ttail_mem (et et' : colseq) : Color0 \notin et -> reflect (et' = et) (ctree_mem (ctree_of_ttail et) et').
proof: Proof. elim: et et' => [|e et IHet] et' /=; first by case: et'; constructor. rewrite inE => /norP[/eqP nz_e nz_et]; rewrite ctree_cons_e_spec ctree_mem_cons. case: et' => [|e' et'] /=; first by right. case De': e'; do [by right=> [] [] | rewrite ctree_mem_sel /= -{}De']; do [case: (e' =P e) => [<- | ]; last by right=> [] []]; by apply: (iffP (IHet _ nz_et)) => [|[]] ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)