proposition: Lemma ctree_cons_e_proper h e t : ctree_proper h t -> ctree_proper h.+1 (ctree_cons_e e t).
proof: Proof. by move=> t_ok; rewrite ctree_cons_e_spec; apply: ctree_cons_proper; case: e. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)