`iIntros "%"` no longer works with universal quantification

This test used to pass until yesterday, but got broken by !400 (merged):

Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.

Lemma test_iIntros_forall_pure P :
  ⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.