Add `big_sepM2_union_inv_*`.

See merge request !690

Thank you, Robbert.

Nested big-op lemmas

See merge request !673

FromPure instances for big_sepM

See merge request iris/iris!626

better error when iMod/iModIntro fails due to mask mismatch

See merge request !691

Add lemmas `big_sepM2_inv_{l,r}` and rename `big_sepM2_lookup_{1,2}` into `big_sepM2_lookup_{l,r}`.

See merge request !692

Add lemmas `big_sepM2_delete_{l,r}` and rename `big_sepM2_lookup_{1,2}` into `big_sepM2_lookup_{l,r}`.

Document `iInduction ... using` tactic.

See merge request iris/iris!682

Explicit visibility for Instances

See merge request !684