Fix IL1 proofs
Working on proofs