proposition: Lemma match_count_eq (st st' : spec_gtree) : st =1 st' -> match_count st =2 match_count st'.
proof: Proof. move=> eq_st bs et; elim: et => [|e et IHet] in st st' eq_st bs *. by rewrite /= eq_st. case: e => //=; try (case: bs => *; congr (_ + _)); by apply: IHet => w; apply: eq_st. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)