Got rid of quantification over number of steps in EENI and LLNI

... but slightly broke Arthur's proofs in the process.