Make `iClear` work when there is at least one absorbing spatial hypothesis
iClear "H"
with H : P
currently works if either the goal is absorbing, or P
is affine. (The same applies to iIntros "_"
).
We could add another case: there exists at least one spatial hypothesis that is absorbing.
See also the discussion in !98 (closed) for a possible use-case.