Better instance for `IntoWand` of `∀ _ : φ, P`
This MR makes sure that iSpecialize
on ∀ _ : φ, P
behaves the same as ⌜ φ ⌝ → P
, which in turn was designed to behave the same as <affine> φ -∗ P
. Similar to ⌜ φ ⌝ → P
, affine modalities are only added in a general BI, not in an affine BI.
The old behavior was that ∀ _ : φ, P
was consider equivalent to φ -∗ P
, but that required P
to be absorbing. That seems like a weird condition...
The tests are variants of those we have for ⌜ φ ⌝ → P
.
This fixes issue #492 (closed).
Edited by Robbert Krebbers