Simplify and update

- evmap is dropped
- per-item invariant is implemented with inv-in-inv
- peritem.v is simplified by proving an ad-hoc iter spec
- update to latest iris
- related fixes
1 job for master in 7 minutes and 4 seconds
Status Job ID Name Coverage
  Test
passed #2056
iris_atomic-coq8.5.3

00:07:04