Clean up `tests/ipm_paper`.
The current iInv
tactic implements exactly the rule that is in the paper, so
let us use that instead of a custom lemma. Back in the days, the iInv
tactic
would put an update modality in the context, so that did not match the paper.