fact: Fixpoint gtr_match0 r := match r with | GtrNil => false | GtrCons _ (CtreeNode _ (CtreeLeaf _) _) _ => true | GtrCons _ (CtreeNode _ _ (CtreeLeaf _)) _ => true | GtrCons _ _ r' => gtr_match0 r' end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)