proposition: Lemma process_eval_rec2_correct f res l : process_eval_rec2 f res l = process_eval_rec1 f res l.
proof: Proof. elim: l res => //= i l IH res. by case: (f i); case: res; rewrite /= ?process_eval_rec1_loss. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)