Skip to content
Snippets Groups Projects
Commit 58e8818d authored by Lennard Gäher's avatar Lennard Gäher
Browse files

change name to gset_bij_elem_of

parent 5941b28a
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment