proposition: Lemma ctree_of_ttail_proper h (et : colseq) : size et = h -> ctree_proper h (ctree_of_ttail et).
proof: Proof. by move <-; elim: et => // e et IHet; apply: ctree_cons_e_proper. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)