From e6d61427fb238eaec2a60786726c29f01e60e555 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Mon, 10 Dec 2018 12:20:50 +0100
Subject: [PATCH] A version of `to_agree_uninj` in the logic.
---
theories/algebra/agree.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 171bc5bf..355f976b 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -241,6 +241,9 @@ Proof.
Qed.
Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y.
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
+
+Lemma to_agree_uninjI {M} x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x.
+Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
End agree.
Instance: Params (@to_agree) 1.
--
GitLab