proposition: Lemma eval_recS n t b : (depth b <= n)%N -> eval_rec n.+1 t b = eval_rec n t b.
proof: Proof. elim: n t b => [/=|n IH] t b Hd. by case: ieval (depth_ieval t b) Hd => //; case: depth. rewrite !eval_recE; case: ieval => //. elim: moves (@moves_depth t b) => [_ |b1 bs IH1 H1d]. by rewrite /= !big_nil. lazy zeta in IH1 |- *; rewrite !big_cons !sflip_min. rewrite IH ?IH1 //. by move=> b2 Hb2; apply: H1d; rewrite in_cons Hb2 orbT. rewrite H1d; last by rewrite in_cons eqxx. by rewrite -ltnS; case: depth Hd. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)