From d317f129db3b7f9c68496c79af73feeaf9de8066 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Aug 2018 00:02:03 +0200
Subject: [PATCH] Update lemma for frac_auth with fraction 1.
---
theories/algebra/frac_auth.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index fdee147fe..08fc6f9e0 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -105,4 +105,9 @@ Section frac_auth.
Proof.
intros. by apply auth_update, option_local_update, prod_local_update_2.
Qed.
+
+ Lemma frac_auth_update_1 a b a' : ✓ a' → â—! a â‹… â—¯! b ~~> â—! a' â‹… â—¯! a'.
+ Proof.
+ intros. by apply auth_update, option_local_update, exclusive_local_update.
+ Qed.
End frac_auth.
--
GitLab