fix lock spec code depending on Σ

See merge request iris/iris!979

rw_lock: add Proper instances

See merge request iris/iris!978

Added IntoPure instance to simplify internal bi equalities into a pure leibniz equality.

See merge request iris/iris!966

make lock spec a Class

See merge request iris/iris!929

Style tweaks to rwlocks.

See merge request iris/iris!977

- Remove unneeded imports
- Remove double spaces and insert space before colons
- Shorten long lines
- Favor `(.. & .. & ..)` over nesting `[.. [.. ..]]`
- Use `injection` intro patterns
- Favor `%H` over `"%H"`
- Use `first by eauto` instead of `first eauto` since the latter does not fail if `eauto` fails

style guide: never put Require in the middle of a file

See merge request iris/iris!973

Add Plain instance for bupd

See merge request iris/iris!975

Internal fractional tweaks.

See merge request iris/iris!976

make iApply greatest_fixpoint_paco work in more cases

See merge request iris/iris!967

- Add `Params` instance and `Proper` instances
- Use `tc_opaque` to prevent `iFrame`/`iNext` from unfolding
- Use `∗-∗` in `iff` lemma to remove `BiAffine`.

fix a lemma being accidentally about the wrong fixpoint...

See merge request iris/iris!974