Add lemma `big_sepM2_alt_dom`.

See merge request iris/iris!938

Rename old lemma into `big_sepM2_alt_lookup`.

Add style point on branching patterns

See merge request iris/iris!927

Fix bug in hint for `AsIdentName` when term is not a lambda.

See merge request iris/iris!936

This style point came up in the feedback on #923, where a lack of
explicit branching in a pattern made a proof more confusing.

I've also moved another pattern-based style point into the newly-created
section just to take advantage of the increased organisation.

Hint to introduce BI version of ``.

See merge request iris/iris!934

Remove weird @

See merge request iris/iris!935

rename_by_string: avoid revert-intros hack

See merge request iris/iris!920

Revert "Merge branch 'ralf/separable' into 'master'"

See merge request !924

This reverts merge request !881

add lemmas for 'separable' propositions

See merge request !881

re-export std++ options

See merge request iris/iris!922