proposition: Lemma eval_rec2_correct n t b : eval_rec2 n t b = eval_rec n t b.
proof: Proof. elim: n t b => //= n IH t b. case: ieval => //. rewrite process_eval_rec2_correct. have /process_eval_rec1_correct : win = \smin_(i <- [::]) (eval_rec2 n (flip t)) i by rewrite big_nil. move=> /(_ (moves t b)); rewrite cats0 => ->. by congr (sflip _); apply: eq_bigr => *; apply: IH. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)