Fix the IL1 proofs

They had broken due to changes in the semantics necessary to get the IL2
proofs through.