From 4664687c52157b96d4f49642703c10b18a5fe3a8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 29 Nov 2021 17:58:30 -0500
Subject: [PATCH] add gmap_view_auth_dfrac_validN

It seems to just have been missed
---
 iris/algebra/lib/gmap_view.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index aa19988e1..6ebf62a34 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -198,6 +198,10 @@ Section lemmas.
     ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 = m2.
   Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
 
+  Lemma gmap_view_auth_dfrac_validN m n dq : ✓{n} gmap_view_auth dq m ↔ ✓ dq.
+  Proof.
+    rewrite view_auth_dfrac_validN. intuition eauto using gmap_view_rel_unit.
+  Qed.
   Lemma gmap_view_auth_dfrac_valid m dq : ✓ gmap_view_auth dq m ↔ ✓ dq.
   Proof.
     rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
-- 
GitLab