A follow up of !836 (merged) to fix two things:

- Various
`Make`

instances still had expensive/recursive/non-constant-time`Affine`

/`Absorbing`

premises. - There were some inconsistencies between the instances for the modalities and the conjunctions, for example, where
`emp ∧ P`

was turned into`P`

if`P`

is affine, but`<affine> P`

remained just`<affine> P`

regardless of whether`P`

is affine.

To fix these things, this MR introduces classes `QuickAffine`

and `QuickAbsorbing`

. These classes are aliases for [Affine] and [Absorbing], but their instances are severely restricted. They only inspect the top-level symbol or check if the whole BI is affine---thus fixing (1). Aside, we use these classes for both all `Make`

instances, thus ensuring consistent behavior and fixing (2).

As a consequence of this MR, one test fails:

```
Lemma demo_3 P1 P2 P3 :
P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
```

What happens is that after framing, the subterm `(P3 ∧ ⌜x = 0⌝) ∨ P3`

is turned into `(emp ∧ ⌜x = 0⌝) ∨ emp`

. Before, the instance for `∨`

would be fired, since `emp ∧ ⌜x = 0⌝`

is affine, thus turning the whole subterm into `emp`

. I don't see how we can support this example without performing a recursive search to check if terms are affine.

That said, this test seems artificial/contrived, so I am not bothered that it fails. This MR is an improvement for Iron, due to fixing (2), a single `iSplit`

can be removed somewhere.