From a31e05be39c4e7a4833a2551b81948c03531dba5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 6 Oct 2016 13:12:10 +0200
Subject: [PATCH] Prove soundness result as stated in the appendix.

---
 algebra/upred.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index a0b707174..392e50779 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.
 
-- 
GitLab