[triviality] Clarify funny proof of `tac_twp_cmpxchg_fail`

See merge request iris/iris!738

To avoid confusion from
iris/iris@d2c226e7 (comment 73999).

add big_sepL_take_drop

See merge request iris/iris!734

add big_sep*_sep_2 lemmas for merging bigops via iDestruct

See merge request iris/iris!736

Optimize iIntoEmpValid

See merge request iris/iris!729

With large proof contexts and lemmas with many forall quantifiers,
iIntoEmpValid can become quite slow. This makes it go faster by adding
"fast paths" for the -> and forall cases, gated by Ltac pattern
matching (which is faster than trying to unify with refine and fail).

Fix and improve `iSpecialize` auto framing error message.

Closes #432

See merge request iris/iris!730

make binary wand/view shift connectives 'block' formated

See merge request iris/iris!727

This closes issue #432.

na_invariants: deduplicate proof of fresh_inv_name

See merge request iris/iris!728

Debatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet
∅`.

Add generalized implication lemma for big_sepM

See merge request iris/iris!697

suggested by Huge Herbelin