fact: Fixpoint ctr_sub r (et : colseq) {struct r} := if r is CtrCons bs t r' then gtree_sub t bs et + ctr_sub r' et else 0.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)