`done` loops in proofmode

Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.