proposition: Lemma eval5_correct t b : eval5 t b = eval t b.
proof: Proof. rewrite /eval5. by have [_ _ [_ ->]] := eval_rec5_correct t (fun=>fun=> None) (leqnn (depth b)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)