proposition: Lemma evalE t b : eval t b = if ieval t b is some v then v else let t1 := flip t in sflip (\smin_(b1 <- moves t b) eval t1 b1).
proof: Proof. rewrite /eval; case E : depth (depth_ieval t b) (@moves_depth t b) => [|n] /=; case: ieval => //= _ Hd. congr sflip; elim: moves Hd => [|b1 bs IH] Hd. by rewrite !big_nil. rewrite !big_cons IH => [|b2 Hb2]; last by rewrite Hd // in_cons Hb2 orbT. rewrite (eval_rec_stable _ (_ : depth b1 <= depth b1 <= n)%nat) //. by rewrite leqnn Hd ?leqnn // in_cons eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)