Update lemma for frac_auth with fraction 1.

d317f129 · Robbert Krebbers · 063be1ab · d317f129
Commit d317f129 authored Aug 02, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

theories/algebra/frac_auth.v theories/algebra/frac_auth.v +5 -0

No files found.
--- 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.