proposition: Lemma ctree_proper_leaf_of_val lf : ctree_proper 0 lf -> lf = ctree_leaf_of (ctree_sub lf [::]).
proof: Proof. by elim: lf => //= lf IHlf /IHlf<-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)