Re-organise the inferencer proof

I wrote it originally in a desparate rush before the POPL deadline, so
it wasn't very organised.