That's fine, we just change the problem from "find a lean proof of length < f(n)" to "find a lean proof that can be validated in time < f(n)".

Oh that’s unfortunate.