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

Printing improvements

See merge request iris/iris!726

use iris.proofmode.proofmode as the new root module for the proofmode

See merge request iris/iris!724

to avoid bad regressions, some other notations also ha to be tweaked