proposition: Lemma eval_draw t b1 b2 : b2 \in moves t b1 -> eval (flip t) b2 = draw -> (forall b, b \in moves t b1 -> eval (flip t) b = draw \/ eval (flip t) b = win) -> eval t b1 = draw.
proof: Proof. move=> b2I Hb2 H; rewrite evalE. case: ieval (liveness t b1) => /= [s /(@sym_equal _ _ _) /negbT|_]. by rewrite negbK => /eqP H1; rewrite H1 in b2I. elim: moves H b2I => //= b3 bs IH H. rewrite big_cons sflip_min in_cons => /orP[/eqP<-| /IH->]; last first. - by move=> b4 Hb4; apply: H; rewrite in_cons Hb4 orbT. - by case (H b3) => [|-> |->] //; rewrite in_cons eqxx. rewrite Hb2. elim: (bs) H => [|b4 {IH}bs IH H]; first by rewrite big_nil. rewrite big_cons sflip_min smaxA [smax (sflip _) _]smaxC -smaxA IH //. by case: (H b4) => [|->|->] //; rewrite !in_cons eqxx orbT. move=> b5 Hb5; apply: H; rewrite !in_cons orbA [(b5 == _) || _]orbC -orbA. by rewrite -in_cons Hb5 orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)