## Define logic `clProp` for axiom-free classical logic + remove `pure_forall_2` from BI interface

This MR defines a new logic `clProp`

that embeds classical logic into Coq. It uses essentially the Gödel-Gentzen translation, so the propositions of `clProp`

are defined as the subset of `Prop`

propositions that are stable under double negation, and the pure, ∨, ∃ connectives of `clProp`

are defined using a double negation.

The logic `clProp`

is a BI, so this MR allows one to use the proof mode to carry out proofs in classical logic, without axioms! For example:

```
Lemma test_excluded_middle P Q : ⊢ P ∨ ¬P.
Proof.
iApply clProp.dn; iIntros "#H". iApply "H".
iRight. iIntros "HP". iApply "H". auto.
Qed.
Lemma test_peirces_law P Q : ((P → Q) → P) ⊢ P.
Proof.
iIntros "#H". iApply clProp.dn; iIntros "#HnotP". iApply "HnotP".
iApply "H". iIntros "HP". iDestruct ("HnotP" with "HP") as %[].
Qed.
```

Unfortunately, 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.