fact: Fixpoint eval_rec4 n t alpha beta b := if ieval t b is some v then s2es v else if n is n1.+1 then process_eval_rec4 (eval_rec4 n1 (flip t)) (esflip beta) (esflip alpha) win (moves t b) else edraw.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)