proposition: Lemma gamesE4 s1 b1 n d s gl v m ms1 b st : next_board n s gl v m b = vresult s1 b1 -> games n d s1 gl v ms1 b1 (b2s d n b1) -> games n d s gl v (m :: ms1) b st.
proof: Proof. intros H; simpl; rewrite H; auto. Qed.
imports: Ascii String List EqNat NArith