diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 22c3b7f9aa688ebb08ad1a8265638dfb548db174..2c628625d0f8ae1ffbe7acfa07cbc25887121620 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -509,7 +509,7 @@ Proof.
     intros P Q.
     unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
   - (* P ⊢ ▷ P *)
-    intros P. unseal; split=> n x ? HP. destruct n; first done. simpl.
+    intros P. unseal; split=> -[|n] /= x ? HP; first done.
     apply uPred_mono with (S n) x; eauto using cmra_validN_S.
   - (* (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a *)
     intros A Φ. unseal; by split=> -[|n] x.