diff --git a/algebra/upred.v b/algebra/upred.v
index a0b70717465f4bd0844d2286384e8737ff29a7fc..392e5077907b8b600da4a1abb76c8d32ec3d6f26 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1492,7 +1492,10 @@ Proof.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 Qed.
 
-Theorem soundness : ¬ (True ⊢ False).
+Corollary soundnessN n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False).
+Proof. exact (adequacy False n). Qed.
+
+Corollary soundness : ¬ (True ⊢ False).
 Proof. exact (adequacy False 0). Qed.
 End uPred_logic.