diff --git a/Iris/Iris/Algebra/Lib.lean b/Iris/Iris/Algebra/Lib.lean
index 30d76e7d6..57bc015ab 100644
--- a/Iris/Iris/Algebra/Lib.lean
+++ b/Iris/Iris/Algebra/Lib.lean
@@ -4,4 +4,5 @@ public import Iris.Algebra.Lib.DFracAgree
 public import Iris.Algebra.Lib.ExclAuth
 public import Iris.Algebra.Lib.FracAuth
 public import Iris.Algebra.Lib.MonoNat
+public import Iris.Algebra.Lib.SetBij
 public import Iris.Algebra.Lib.UFracAuth
diff --git a/Iris/Iris/Algebra/Lib/SetBij.lean b/Iris/Iris/Algebra/Lib/SetBij.lean
new file mode 100644
index 000000000..da792110d
--- /dev/null
+++ b/Iris/Iris/Algebra/Lib/SetBij.lean
@@ -0,0 +1,217 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors:
+-/
+module
+
+public import Iris.Algebra.LeibnizSet
+public import Iris.Algebra.View
+public import Iris.Algebra.Updates
+meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+/-!
+# RA for monotone partial bijections
+
+This RA is a view where the authoritative element is a partial bijection between types `A` and `B`
+and the fragments are subrelations of the bijection. The data for the bijection is represented as a
+set of pairs `A × B`, and the view relation enforces that when an authoritative element is valid it
+is a bijection (that is, it is deterministic as a function from `A → Option B` and `B → Option A`).
+
+The fragments compose by set union, which means that fragments are their own core, ownership of a
+fragment is persistent, and the authoritative element can only grow (in that it can only map more
+pairs `(a, b)`).
+
+As with `LeibnizSet`, the set of pairs is not fixed to a concrete representation: the construction
+is generic in any `LawfulSet S (A × B)`.
+-/
+
+namespace Iris
+
+open Std CMRA OFE LawfulSet LeibnizSet View
+
+variable {S A B : Type _} [LawfulSet S (A × B)]
+variable {a a₁ a₂ : A} {b b₁ b₂ : B} {L L' L₁ L₂ : S} {dq dq₁ dq₂ : DFrac}
+
+/-- `SetBijective L` states that for a graph `L` of `(a, b)` pairs, `L` maps from `A` to `B` and
+back deterministically. The key property characterizing `SetBijective` is `SetBijective.eq_iff`. -/
+@[rocq_alias gset_bijective]
+def SetBijective (L : S) : Prop :=
+  ∀ a b, (a, b) ∈ L → (∀ b', (a, b') ∈ L → b' = b) ∧ (∀ a', (a', b) ∈ L → a' = a)
+
+namespace SetBijective
+
+@[rocq_alias gset_bijective_empty]
+theorem empty : SetBijective (∅ : S) := fun _ _ h => absurd h mem_empty
+
+/-- A bijective graph `L` can be extended with a new mapping `(a, b)` as long as neither `a` nor
+`b` is currently mapped to anything. -/
+@[rocq_alias gset_bijective_extend]
+theorem extend (hL : SetBijective L) (ha : ∀ b', (a, b') ∉ L) (hb : ∀ a', (a', b) ∉ L) :
+    SetBijective ({(a, b)} ∪ L) := by
+  rw [← insert_union]
+  intro a₁ b₁ h₁
+  rw [mem_insert, Prod.mk.injEq] at h₁
+  refine ⟨fun b₂ h₂ => ?_, fun a₂ h₂ => ?_⟩ <;>
+    rw [mem_insert, Prod.mk.injEq] at h₂ <;> obtain ⟨rfl, rfl⟩ | h₁ := h₁
+  · exact h₂.elim (·.2) (absurd · (ha b₂))
+  · exact h₂.elim (fun h => absurd (h.1 ▸ h₁) (ha b₁)) fun h₂ => (hL _ _ h₁).1 b₂ h₂
+  · exact h₂.elim (·.1) (absurd · (hb a₂))
+  · exact h₂.elim (fun h => absurd (h.2 ▸ h₁) (hb a₁)) fun h₂ => (hL _ _ h₁).2 a₂ h₂
+
+@[rocq_alias gset_bijective_eq_iff]
+theorem eq_iff (hL : SetBijective L) (h₁ : (a₁, b₁) ∈ L) (h₂ : (a₂, b₂) ∈ L) :
+    a₁ = a₂ ↔ b₁ = b₂ := by
+  refine ⟨?_, ?_⟩ <;> rintro rfl
+  · exact ((hL _ _ h₁).1 _ h₂).symm
+  · exact ((hL _ _ h₁).2 _ h₂).symm
+
+@[rocq_alias gset_bijective_pair]
+theorem pair (h : SetBijective ({(a₁, b₁), (a₂, b₂)} : S)) : a₁ = a₂ ↔ b₁ = b₂ :=
+  h.eq_iff (mem_insert.mpr (.inl rfl)) (mem_insert.mpr (.inr (mem_singleton.mpr rfl)))
+
+@[rocq_alias subseteq_gset_bijective]
+theorem mono (hL : SetBijective L) (h : L' ⊆ L) : SetBijective L' := fun a b hab =>
+  ⟨fun b' h' => (hL a b (mem_of_subset h hab)).1 b' (mem_of_subset h h'),
+   fun a' h' => (hL a b (mem_of_subset h hab)).2 a' (mem_of_subset h h')⟩
+
+end SetBijective
+
+namespace SetBij
+
+/-- The view relation: a fragment is a subrelation of the authoritative bijection. -/
+@[rocq_alias gset_bij_view_rel, rocq_alias gset_bij_view_rel_raw]
+def viewRel : ViewRel (LeibnizSet S) (LeibnizSet S)
+  | _, valid bijL, valid L => L ⊆ bijL ∧ SetBijective bijL
+
+@[rocq_alias gset_bij_view_rel_iff]
+theorem viewRel_iff {n} : viewRel n (valid L') (valid L) ↔ L ⊆ L' ∧ SetBijective L' := .rfl
+
+@[rocq_alias gset_bij_view_rel_raw_mono, rocq_alias gset_bij_view_rel_raw_valid,
+  rocq_alias gset_bij_view_rel_raw_unit]
+instance : IsViewRel (viewRel (S := S)) where
+  mono {_ x₁ y₁ n₂ x₂ y₂} h hx hy _ := by
+    obtain ⟨_⟩ := x₁
+    obtain ⟨_⟩ := x₂
+    obtain ⟨_⟩ := y₁
+    obtain ⟨_⟩ := y₂
+    injection (hx : _ = _) with hx
+    subst hx
+    exact ⟨subset_trans ((included_iff_subset ..).mp ((inc_iff_incN n₂).mpr hy)) h.1, h.2⟩
+  rel_validN _ _ _ _ := trivial
+  rel_unit _ := ⟨valid ∅, subset_refl, .empty⟩
+
+@[rocq_alias gset_bij_view_rel_discrete]
+instance : IsViewRelDiscrete (viewRel (S := S)) where
+  discrete _ _ _ h := h
+
+end SetBij
+
+/-- The RA of monotone partial bijections over a set `S` of pairs. -/
+@[rocq_alias gset_bij, rocq_alias gset_bijO, rocq_alias gset_bijR, rocq_alias gset_bijUR]
+abbrev SetBij (S : Type _) [LawfulSet S (A × B)] := View (SetBij.viewRel (S := S))
+
+namespace SetBij
+
+@[rocq_alias gset_bij_auth]
+def auth (dq : DFrac) (L : S) : SetBij S := (●V{dq} valid L) • ◯V valid L
+
+@[rocq_alias gset_bij_elem]
+def elem (a : A) (b : B) : SetBij S := ◯V valid {(a, b)}
+
+@[rocq_alias gset_bij_elem_core_id]
+instance : CoreId (elem a b : SetBij S) := inferInstanceAs (CoreId (◯V _))
+
+theorem frag_op_union : ((◯V valid L₁ : SetBij S) • ◯V valid L₂) = ◯V valid (L₁ ∪ L₂) := by
+  rw [← frag_op_eq, op_union]
+
+/-- The authoritative and fragment parts of two `auth`s, regrouped. -/
+theorem auth_op_auth_eq : ((auth dq₁ L₁ : SetBij S) • auth dq₂ L₂)
+    = ((●V{dq₁} valid L₁ : SetBij S) • ●V{dq₂} valid L₂) • ◯V valid (L₁ ∪ L₂) := by
+  rw [auth, auth, ← frag_op_union, ← assoc_L, assoc_L (x := (◯V valid L₁ : SetBij S)),
+    comm_L (x := (◯V valid L₁ : SetBij S)), ← assoc_L, assoc_L]
+
+@[rocq_alias gset_bij_auth_dfrac_op]
+theorem auth_op_auth : ((auth dq₁ L : SetBij S) • auth dq₂ L) = auth (dq₁ • dq₂) L := by
+  rw [auth_op_auth_eq, union_idem, ← auth_op_auth_eqv, auth]
+
+@[rocq_alias gset_bij_auth_dfrac_valid]
+theorem auth_valid_iff : ✓ (auth dq L : SetBij S) ↔ ✓ dq ∧ SetBijective L := by
+  rw [auth, auth_op_frag_valid_iff]
+  exact and_congr_right fun _ => ⟨fun h => (h 0).2, fun h _ => ⟨subset_refl, h⟩⟩
+
+@[rocq_alias gset_bij_auth_valid]
+theorem auth_one_valid_iff : ✓ (auth (.own 1) L : SetBij S) ↔ SetBijective L :=
+  auth_valid_iff.trans <| and_iff_right_iff_imp.mpr fun _ => DFrac.valid_own_one
+
+@[rocq_alias gset_bij_auth_empty_dfrac_valid]
+theorem auth_empty_valid_iff : ✓ (auth dq (∅ : S) : SetBij S) ↔ ✓ dq :=
+  auth_valid_iff.trans <| and_iff_left_iff_imp.mpr fun _ => .empty
+
+@[rocq_alias gset_bij_auth_empty_valid]
+theorem auth_one_empty_valid : ✓ (auth (.own 1) (∅ : S) : SetBij S) :=
+  auth_empty_valid_iff.mpr DFrac.valid_own_one
+
+@[rocq_alias gset_bij_auth_dfrac_op_valid]
+theorem auth_op_auth_valid_iff : ✓ ((auth dq₁ L₁ : SetBij S) • auth dq₂ L₂)
+    ↔ ✓ (dq₁ • dq₂) ∧ L₁ = L₂ ∧ SetBijective L₁ := by
+  rw [auth_op_auth_eq]
+  refine ⟨fun h => ?_, fun ⟨hdq, rfl, hbij⟩ => ?_⟩
+  · obtain ⟨hdq, hL, hrel⟩ := View.auth_op_auth_valid_iff.mp (valid_op_left h)
+    injection hL with hL
+    exact ⟨hdq, hL, (hrel 0).2⟩
+  · rw [union_idem, ← auth_op_auth_eqv]
+    exact auth_op_frag_valid_iff.mpr ⟨hdq, fun _ => ⟨subset_refl, hbij⟩⟩
+
+@[rocq_alias gset_bij_auth_op_valid]
+theorem auth_one_op_auth_one_valid_iff :
+    ✓ ((auth (.own 1) L₁ : SetBij S) • auth (.own 1) L₂) ↔ False := by
+  rw [auth_op_auth_eq]
+  exact ⟨fun h => View.auth_one_op_auth_one_valid_iff.mp (valid_op_left h), False.elim⟩
+
+@[rocq_alias bij_both_dfrac_valid]
+theorem auth_op_elem_valid_iff : ✓ ((auth dq L : SetBij S) • elem a b)
+    ↔ ✓ dq ∧ SetBijective L ∧ (a, b) ∈ L := by
+  rw [auth, elem, ← assoc_L, frag_op_union, auth_op_frag_valid_iff]
+  refine and_congr_right fun _ => ⟨fun h => ⟨(h 0).2, ?_⟩, fun ⟨hbij, hmem⟩ _ => ⟨?_, hbij⟩⟩
+  · exact mem_of_subset (h 0).1 (mem_union.mpr (.inr (mem_singleton.mpr rfl)))
+  · intro x hx
+    obtain hx | hx := mem_union.mp hx
+    · exact hx
+    · rw [mem_singleton.mp hx]
+      exact hmem
+
+@[rocq_alias bij_both_valid]
+theorem auth_one_op_elem_valid_iff : ✓ ((auth (.own 1) L : SetBij S) • elem a b)
+    ↔ SetBijective L ∧ (a, b) ∈ L :=
+  auth_op_elem_valid_iff.trans <| and_iff_right_iff_imp.mpr fun _ => DFrac.valid_own_one
+
+@[rocq_alias gset_bij_elem_agree]
+theorem elem_agree (h : ✓ ((elem a₁ b₁ : SetBij S) • elem a₂ b₂)) : a₁ = a₂ ↔ b₁ = b₂ := by
+  rw [elem, elem, frag_op_union, frag_valid_iff] at h
+  obtain ⟨⟨bijL⟩, hsub, hbij⟩ := h 0
+  refine SetBijective.pair (S := S) ?_
+  rw [insert_union]
+  exact hbij.mono hsub
+
+@[rocq_alias bij_view_included]
+theorem elem_inc_auth (h : (a, b) ∈ L) : (elem a b : SetBij S) ≼ auth dq L :=
+  inc_trans (frag_inc_of_inc <| (included_iff_subset ..).mpr fun _ hx => mem_singleton.mp hx ▸ h)
+    (inc_op_right ..)
+
+@[rocq_alias gset_bij_auth_extend]
+theorem auth_extend (ha : ∀ b', (a, b') ∉ L) (hb : ∀ a', (a', b) ∉ L) :
+    (auth (.own 1) L : SetBij S) ~~> auth (.own 1) ({(a, b)} ∪ L) := by
+  refine auth_one_op_frag_update fun _ bf h => ?_
+  obtain ⟨_⟩ := bf
+  rw [op_union] at h ⊢
+  refine ⟨fun x hx => ?_, h.2.extend ha hb⟩
+  obtain hx | hx := mem_union.mp hx
+  · exact hx
+  · exact mem_union.mpr (.inr (mem_of_subset h.1 (mem_union.mpr (.inr hx))))
+
+end SetBij
+
+end Iris
diff --git a/Iris/Iris/Instances/Lib.lean b/Iris/Iris/Instances/Lib.lean
index b29c784ca..49f05deaa 100644
--- a/Iris/Iris/Instances/Lib.lean
+++ b/Iris/Iris/Instances/Lib.lean
@@ -9,5 +9,6 @@ public import Iris.Instances.Lib.Invariants
 public import Iris.Instances.Lib.LaterCredits
 public import Iris.Instances.Lib.NaInvariants
 public import Iris.Instances.Lib.SavedProp
+public import Iris.Instances.Lib.SetBij
 public import Iris.Instances.Lib.Token
 public import Iris.Instances.Lib.WSat
diff --git a/Iris/Iris/Instances/Lib/SetBij.lean b/Iris/Iris/Instances/Lib/SetBij.lean
new file mode 100644
index 000000000..5e5980f07
--- /dev/null
+++ b/Iris/Iris/Instances/Lib/SetBij.lean
@@ -0,0 +1,229 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors:
+-/
+module
+
+public import Iris.Algebra.Lib.SetBij
+public import Iris.BI.BigOp.BigSepSet
+public import Iris.BI.Lib.Fractional
+public import Iris.Instances.IProp
+public import Iris.ProofMode
+meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+/-!
+# Propositions for reasoning about monotone partial bijections
+
+This library provides two propositions `set_bij_own_auth γ dq L` and `set_bij_own_elem γ a b`,
+where `L` is a bijection between types `A` and `B` represented by a set `S` of associations
+`A × B`. The idea is that `set_bij_own_auth γ dq L` is an authoritative bijection `L`, while
+`set_bij_own_elem γ a b` is a persistent resource saying `L` associates `a` and `b`.
+
+The main use case is in a logical relation-based proof where `L` maintains the association between
+locations `A` in one execution and `B` in another (perhaps of different types, if the logical
+relation relates two different semantics).
+
+The association `L` is always bijective, so that if `a` is mapped to `b`, there should be no other
+mappings for either `a` or `b`; the `set_bij_own_extend` update theorem enforces that new mappings
+respect this property, and `set_bij_own_elem_agree` allows the user to exploit bijectivity. The
+bijection grows monotonically, so that the set of associations only grows; this is captured by the
+persistence of `set_bij_own_elem`.
+
+This library is a logical, ownership-based wrapper around `SetBij`.
+-/
+
+namespace Iris
+
+open Std CMRA BI ProofMode BigSepS LawfulSet SetBij
+
+@[rocq_alias gset_bijG]
+class SetBijG (GF : BundledGFunctors) (A B : Type _) (S : outParam (Type _))
+    [LawfulSet S (A × B)] where
+  elem : ElemG GF (constOF (SetBij S))
+
+attribute [reducible, instance] SetBijG.elem
+
+#rocq_ignore «gset_bijΣ» "Subsumed by BundledGFunctors typeclass synthesis"
+#rocq_ignore «subG_gset_bijΣ» "Subsumed by BundledGFunctors typeclass synthesis"
+
+section definitions
+
+variable {A B S : Type _} [LawfulSet S (A × B)] [SetBijG GF A B S]
+
+@[rocq_alias gset_bij_own_auth]
+public def set_bij_own_auth (γ : GName) (dq : DFrac) (L : S) : IProp GF :=
+  iOwn (E := SetBijG.elem) γ (auth dq L)
+
+@[rocq_alias gset_bij_own_elem]
+public def set_bij_own_elem (γ : GName) (a : A) (b : B) : IProp GF :=
+  iOwn (E := SetBijG.elem) γ (elem (S := S) a b)
+
+#rocq_ignore gset_bij_own_auth_def "Not needed"
+#rocq_ignore gset_bij_own_auth_aux "Not needed"
+#rocq_ignore gset_bij_own_auth_eq "Not needed"
+#rocq_ignore gset_bij_own_elem_def "Not needed"
+#rocq_ignore gset_bij_own_elem_aux "Not needed"
+#rocq_ignore gset_bij_own_elem_eq "Not needed"
+
+end definitions
+
+notation γ " ↪●BIJ{" dq "} " L => set_bij_own_auth γ dq L
+notation γ " ↪●BIJ " L => set_bij_own_auth γ (DFrac.own 1) L
+notation γ " ↪◯BIJ⟨" a ", " b "⟩" => set_bij_own_elem γ a b
+
+section lemmas
+
+variable {A B S : Type _} [LawfulSet S (A × B)] [SetBijG GF A B S]
+variable {γ : GName} {dq dq₁ dq₂ : DFrac} {L L₁ L₂ : S}
+
+@[rocq_alias gset_bij_own_auth_timeless]
+instance : Timeless (PROP := IProp GF) (γ ↪●BIJ{dq} L) := by
+  unfold set_bij_own_auth
+  infer_instance
+
+@[rocq_alias gset_bij_own_auth_persistent]
+instance : Persistent (PROP := IProp GF) (γ ↪●BIJ{.discard} L) := by
+  unfold set_bij_own_auth auth
+  infer_instance
+
+@[rocq_alias gset_bij_own_elem_timeless]
+instance (a : A) (b : B) : Timeless (PROP := IProp GF) (γ ↪◯BIJ⟨a, b⟩) := by
+  unfold set_bij_own_elem
+  infer_instance
+
+@[rocq_alias gset_bij_own_elem_persistent]
+instance (a : A) (b : B) : Persistent (PROP := IProp GF) (γ ↪◯BIJ⟨a, b⟩) := by
+  unfold set_bij_own_elem
+  infer_instance
+
+@[rocq_alias gset_bij_own_auth_fractional]
+instance : Fractional (PROP := IProp GF) fun q => γ ↪●BIJ{.own q} L where
+  fractional p q := by
+    unfold set_bij_own_auth
+    refine .trans ?_ iOwn_op
+    refine BIBase.BiEntails.of_eq ?_
+    exact congrArg (iOwn γ) (auth_op_auth (dq₁ := .own p) (dq₂ := .own q) (L := L)).symm
+
+@[rocq_alias gset_bij_own_auth_as_fractional]
+instance (q : Qp) : AsFractional (PROP := IProp GF) (γ ↪●BIJ{.own q} L)
+    ioΦ (fun q => γ ↪●BIJ{.own q} L) ioq q where
+  as_fractional := .rfl
+  as_fractional_fractional := inferInstance
+
+@[rocq_alias gset_bij_own_auth_agree]
+theorem set_bij_own_auth_agree :
+    (γ ↪●BIJ{dq₁} L₁) ∗ (γ ↪●BIJ{dq₂} L₂) ⊢@{IProp GF}
+      ⌜✓ (dq₁ • dq₂) ∧ L₁ = L₂ ∧ SetBijective L₁⌝ := by
+  unfold set_bij_own_auth
+  iintro ⟨H1, H2⟩
+  icombine H1 H2 gives %H
+  ipureintro
+  exact auth_op_auth_valid_iff.mp H
+
+@[rocq_alias gset_bij_own_auth_exclusive]
+theorem set_bij_own_auth_exclusive : (γ ↪●BIJ L₁) ∗ (γ ↪●BIJ L₂) ⊢@{IProp GF} False := by
+  unfold set_bij_own_auth
+  iintro ⟨H1, H2⟩
+  icombine H1 H2 gives %H
+  exact (auth_one_op_auth_one_valid_iff.mp H).elim
+
+@[rocq_alias gset_bij_own_valid]
+theorem set_bij_own_valid : (γ ↪●BIJ{dq} L) ⊢@{IProp GF} ⌜✓ dq ∧ SetBijective L⌝ := by
+  unfold set_bij_own_auth
+  refine iOwn_cmraValid.trans ?_
+  iintro %h
+  ipureintro
+  exact auth_valid_iff.mp h
+
+@[rocq_alias gset_bij_own_elem_agree]
+theorem set_bij_own_elem_agree (a a' : A) (b b' : B) :
+    (γ ↪◯BIJ⟨a, b⟩) ∗ (γ ↪◯BIJ⟨a', b'⟩) ⊢@{IProp GF} ⌜a = a' ↔ b = b'⌝ := by
+  unfold set_bij_own_elem
+  iintro ⟨H1, H2⟩
+  icombine H1 H2 gives %H
+  ipureintro
+  exact elem_agree H
+
+@[rocq_alias gset_bij_own_elem_get]
+theorem set_bij_own_elem_get (a : A) (b : B) (h : (a, b) ∈ L) :
+    (γ ↪●BIJ{dq} L) ⊢@{IProp GF} γ ↪◯BIJ⟨a, b⟩ :=
+  iOwn_mono (elem_inc_auth h)
+
+@[rocq_alias gset_bij_elem_of]
+theorem set_bij_elem_of (a : A) (b : B) :
+    (γ ↪●BIJ{dq} L) ∗ (γ ↪◯BIJ⟨a, b⟩) ⊢@{IProp GF} ⌜(a, b) ∈ L⌝ := by
+  unfold set_bij_own_auth set_bij_own_elem
+  iintro ⟨H1, H2⟩
+  icombine H1 H2 gives %H
+  ipureintro
+  exact (auth_op_elem_valid_iff.mp H).2.2
+
+end lemmas
+
+section finiteLemmas
+
+variable {A B S : Type _} [LawfulFiniteSet S (A × B)] [SetBijG GF A B S]
+variable {γ : GName} {dq : DFrac} {L : S}
+
+@[rocq_alias gset_bij_own_elem_get_big]
+theorem set_bij_own_elem_get_big :
+    (γ ↪●BIJ{dq} L) ⊢@{IProp GF} [∗set] ab ∈ L, γ ↪◯BIJ⟨ab.1, ab.2⟩ := by
+  refine .trans ?_ bigSepS_forall.mpr
+  iintro H %⟨a, b⟩ %hab
+  iapply set_bij_own_elem_get a b hab
+  iexact H
+
+@[rocq_alias gset_bij_own_alloc]
+theorem set_bij_own_alloc (L : S) (h : SetBijective L) :
+    ⊢@{IProp GF} |==> ∃ γ, (γ ↪●BIJ L) ∗ [∗set] ab ∈ L, γ ↪◯BIJ⟨ab.1, ab.2⟩ := by
+  imod (iOwn_alloc (E := SetBijG.elem) (auth (.own 1) L) (auth_one_valid_iff.mpr h)) with ⟨%γ, G⟩
+  imodintro
+  iexists γ
+  iapply persistent_entails_left set_bij_own_elem_get_big
+  iunfold set_bij_own_auth
+  iexact G
+
+@[rocq_alias gset_bij_own_alloc_empty]
+theorem set_bij_own_alloc_empty : ⊢@{IProp GF} |==> ∃ γ, γ ↪●BIJ (∅ : S) := by
+  imod (set_bij_own_alloc (∅ : S) .empty) with ⟨%γ, H, -⟩
+  imodintro
+  iexists γ
+  iexact H
+
+end finiteLemmas
+
+section updates
+
+variable {A B S : Type _} [LawfulSet S (A × B)] [SetBijG GF A B S]
+variable {γ : GName} {L : S}
+
+@[rocq_alias gset_bij_own_extend]
+theorem set_bij_own_extend (a : A) (b : B) (ha : ∀ b', (a, b') ∉ L) (hb : ∀ a', (a', b) ∉ L) :
+    (γ ↪●BIJ L) ⊢@{IProp GF} |==> ((γ ↪●BIJ ({(a, b)} ∪ L)) ∗ γ ↪◯BIJ⟨a, b⟩) :=
+  (iOwn_update (auth_extend ha hb)).trans <| BIUpdate.mono <| persistent_entails_left <|
+    set_bij_own_elem_get a b (mem_union.mpr (.inl (mem_singleton.mpr rfl)))
+
+@[rocq_alias gset_bij_own_extend_internal]
+theorem set_bij_own_extend_internal (a : A) (b : B) :
+    iprop((∀ b' : B, (γ ↪◯BIJ⟨a, b'⟩) -∗ False) ∗ (∀ a' : A, (γ ↪◯BIJ⟨a', b⟩) -∗ False) ∗
+      (γ ↪●BIJ L)) ⊢@{IProp GF} |==> ((γ ↪●BIJ ({(a, b)} ∪ L)) ∗ γ ↪◯BIJ⟨a, b⟩) := by
+  iintro ⟨Ha, Hb, HL⟩
+  ihave %h₁ : ⌜∀ b', (a, b') ∉ L⌝ $$ [Ha HL]
+  · iintro %b' %hmem
+    iapply Ha $$ %b'
+    iapply set_bij_own_elem_get a b' hmem
+    iexact HL
+  ihave %h₂ : ⌜∀ a', (a', b) ∉ L⌝ $$ [Hb HL]
+  · iintro %a' %hmem
+    iapply Hb $$ %a'
+    iapply set_bij_own_elem_get a' b hmem
+    iexact HL
+  iapply set_bij_own_extend a b h₁ h₂
+  iexact HL
+
+end updates
+
+end Iris