Testcase: ```coq Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}: Q ∗ (Q -∗ P) -∗ Q ∗ P. Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". ``` Prints ``` No matching clauses for match. ``` That's never an acceptable error message, obviously.