Std.Natural

How many of f 0, f 1, ..., f (count - 1) are zero: a plain fold over a closed count, so the checker runs it as a strict loop -- one cell at a time, each forgotten once counted. (The first formulation nested each cell's select inside the previous one; a verdict of 40 cells that each run a program kept every earlier cell alive: 51 s against 7.6 s, two thirds of it garbage collection.)

275def naturalFailuresBelow =
276  (lambda unrestricted count : Nat .
277    (lambda unrestricted f : (pi unrestricted index : Nat . Nat) .
278      (nat-eliminate
279        (lambda unrestricted current : Nat . Nat)
280        0
281        (lambda unrestricted predecessor : Nat .
282          (lambda unrestricted induction : Nat . (naturalAdd (naturalIsZero (f predecessor)) induction)))
283        count)))