"not a BI assertion" when using let-bindings
The following script used to work, but was broken by the change to -∗ notation:
Section tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_wand_below_let (P : PROP) :
let Q := (P ∗ P)%I in
Q -∗ Q.
Proof. iIntros "?".
Using ⊢
instead of -∗
still works, but this should also work with a wand.