proposition: Lemma gamesE n d s gl v m ms1 b st : games n d s gl v (m :: ms1) b st = let nb := next_board n s gl v m b in match nb with | iresult => Invalid_Move | lresult => Lost | wresult => Won ms1 | vresult s1 b1 => games n d s1 gl v ms1 b1 (b2s d n b1) end.
proof: Proof. trivial. Qed.
imports: Ascii String List EqNat NArith