Prove different versions of Löb rule

This MR follows a discussion with @dreyer @amintimany and @birkedal about a version of Löb without implication. We came up with □ (▷ P -∗ P) ⊢ P and showed it's equivalent to the normal Löb rule in affine BIs (lemma löb_alt in this MR).

I then spend an hour staring and trying to generalize löb_alt to non-affine BIs, but gave up.

This MR adds the following lemmas:

Lemma löb_wand_intuitionistically `{!BiLöb PROP} P : □ (□ ▷ P -∗ P) ⊢ P.
Lemma löb_wand `{!BiLöb PROP} P : □ (▷ P -∗ P) ⊢ P.
Lemma löb_alt `{!BiAffine PROP} : BiLöb PROP ↔ ∀ P, □ (▷ P -∗ P) ⊢ P.

Also, it shortens the proof of tac_löb via löb_wand_intuitionistically.