proposition: Lemma gtree_empty4P {t0 t1 t2 t3} : reflect (are_4_GtreeEmpty t0 t1 t2 t3) (gtree_empty4 (GtreeNode t0 t1 t2 t3)).
proof: Proof. rewrite /gtree_empty4 3!gtree_empty_and_spec. by apply: (iffP and4P) => [[]|[]//]; do 4!move/gtree_emptyP->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)