proposition: Lemma fold_gtree_empty A (ve vne : A) t : (if t is GtreeEmpty then ve else vne) = (if gtree_empty t then ve else vne).
proof: Proof. by case: t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)