From 58e8818de7af40a4080d73d466cacb764de08a25 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Mon, 19 Apr 2021 10:40:46 +0200
Subject: [PATCH] change name to gset_bij_elem_of

---
 iris/base_logic/lib/gset_bij.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index c45c24475..45f6a84e4 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -114,7 +114,7 @@ Section gset_bij.
     by apply own_mono, bij_view_included.
   Qed.
 
-  Lemma gset_bij_own_both_elem_of {γ q L} a b :
+  Lemma gset_bij_elem_of {γ q L} a b :
     gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b -∗ ⌜(a, b) ∈ L⌝.
   Proof.
     iIntros "Hauth Helem". rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
-- 
GitLab