Remove `pure_forall_2` from BI interface + BI notation for `¬`
This is the non-controversial part of !496 (closed)
The clProp
logic does not enjoy the BI law (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝
. Therefore, I have removed this law from the BI interface, and factored it into a type class BiPureForall
. This follows the same pattern as we use for other properties that do not hold for all BIs.
This is a breaking change for developments that define their own BI instances, but I think the only one out there is Iron.