fact: Fixpoint eval_rec2 n t b := if ieval t b is some v then v else if n is n1.+1 then process_eval_rec2 (eval_rec2 n1 (flip t)) win (moves t b) else draw.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)