Merged requested to merge robbert/loeb_weak into master
This MR adds the lemma:
Lemma löb_weak : BiLöb PROP ↔ ∀ P, (▷ P ⊢ P) → (True ⊢ P).
This lemma was implicit as part of the proof
later_contractive_bi_löb. Since it's an interesting result on its own, I factored it out as a separate lemma. I also stated the result as a bi-implication (the left-to-right implication is trivial, though).
I also improved the comments.