Add notations for `<affine> ⌜ ⌝` and friends.

This MR adds the following notations:

• ⌜⌜ φ ⌝⌝ for <affine> ⌜ φ ⌝
• ⎡⎡ P ⎤⎤ for <affine> ⎡ P ⎤
• x ≡≡ y for <affine> (x ≡ y)
• x ≼≼ y for <affine> (x ≼ y)

So the idea is: doubling the symbol makes it affine. This should also scale to ✓✓ x := <affine> (✓ x), once we have ✓ for any SBI.

I think this is a more feasible alternative to earlier discussions where we planned to make the ordinary notations the affine ones, because:

1. Most users of Iris don't use linear BIs, so the alternative would be an invasive change, whereas the current MR is trivial.
2. Many lemmas don't hold for the affine version. For example f ≡ g ⊣⊢ ∀ x, f x ≡ g x does not hold for ≡≡. So if the affine version is the default, we need to duplicate all our lemmas, similar to how we have duplicated all lemmas for <pers> and □. This sounds like too much work for too little gain. In proofs with the present MR, you would typically move the affine version into the persistent context, thus stripping the affine modality, allowing you to use the lemmas for the non-affine version.
3. Some lemmas would need absorbing modalities for the affine versions. For example own γ x ⊢ ✓ x would not hold in an affine BI if ✓ where affine. (This example only applies once we have a general own and ✓, there might be other examples in our current code-base already).
4. We support instances of Embed where ⎡ P ⎤ is affine and where it is not, so having <affine> ⎡ _ ⎤ as the default would not be desired. For example, the embedding of iProp into ironProp is not affine, so you often want to use ⎡⎡ P ⎤⎤. However, if BiEmbedEmp holds, you want to use ⎡ P ⎤ (without affine modality), so that ⎡ P ⎤ is affine if P is affine.

TODO: Since there are not many uses of these new notations, we should add some tests. In particular, we should test that ⎡ ⎡ P ⎤ ⎤ is not pretty printed as ⎡⎡ P ⎤⎤.