fact: Definition sgtree_partition (st st' st'' : spec_gtree) := forall w, (if st w then eqb else orb) (st' w) (st'' w) = false.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)