diff --git a/src/Iris/BI/Updates.lean b/src/Iris/BI/Updates.lean
index 604f2654..c50c8911 100644
--- a/src/Iris/BI/Updates.lean
+++ b/src/Iris/BI/Updates.lean
@@ -10,17 +10,11 @@ import Iris.BI.Classes
 import Iris.BI.DerivedLaws
 import Iris.Algebra
 import Iris.BI.Plainly
+import Iris.Std.CoPset
 
 namespace Iris
 open Iris.Std BI
 
---TODO: Which type should we use for sets of masks?
-def Set (α : Type _) := α → Prop
-def Set.univ {α : Type _} : Set α := fun _ => True
-def Subset (x y : Set α) : Prop := ∀ a, x a → y a
-def Disjoint (x y : Set α) : Prop := ∀ a, ¬(x a ∧ y a)
-def union (x y : Set α) : Set α := fun a => x a ∨ y a
-
 class BUpd (PROP : Type _) where
   bupd : PROP → PROP
 export BUpd (bupd)
@@ -37,8 +31,8 @@ delab_rule BUpd.bupd
 -- delab_rule WandUpdate ??
 --   | `($_ $P $Q) => ``(iprop($P ==∗ $Q))
 
-class FUpd (PROP : Type _) (MASK : Type _) where
-  fupd : Set MASK → Set MASK → PROP → PROP
+class FUpd (PROP : Type _) where
+  fupd : CoPset → CoPset → PROP → PROP
 export FUpd (fupd)
 
 syntax "|={ " term " , " term " }=> " term : term
@@ -87,26 +81,26 @@ class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
   trans {P : PROP} : iprop(|==> |==> P ⊢ |==> P)
   frame_r {P R : PROP} : iprop((|==> P) ∗ R ⊢ |==> (P ∗ R))
 
-class BIFUpdate (PROP MASK : Type _) [BI PROP] extends FUpd PROP MASK where
-  [ne {E1 E2 : Set MASK} : OFE.NonExpansive (FUpd.fupd E1 E2 (PROP := PROP))]
-  subset {E1 E2 : Set MASK} : Subset E2 E1 → ⊢ |={E1, E2}=> |={E2, E1}=> (emp : PROP)
-  except0 {E1 E2 : Set MASK} (P : PROP) : (◇ |={E1, E2}=> P) ⊢ |={E1, E2}=> P
-  trans {E1 E2 E3 : Set MASK} (P : PROP) : (|={E1, E2}=> |={E2, E3}=> P) ⊢ |={E1, E3}=> P
-  mask_frame_r' {E1 E2 Ef : Set MASK} (P : PROP) :
-    Disjoint E1 Ef → (|={E1,E2}=> ⌜Disjoint E2 Ef⌝ → P) ⊢ |={union E1 Ef, union E2 Ef}=> P
-  frame_r {E1 E2 : Set MASK} (P R : PROP) :
+class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
+  [ne {E1 E2 : CoPset} : OFE.NonExpansive (FUpd.fupd E1 E2 (PROP := PROP))]
+  subset {E1 E2 : CoPset} : Subset E2 E1 → ⊢ |={E1, E2}=> |={E2, E1}=> (emp : PROP)
+  except0 {E1 E2 : CoPset} (P : PROP) : (◇ |={E1, E2}=> P) ⊢ |={E1, E2}=> P
+  trans {E1 E2 E3 : CoPset} (P : PROP) : (|={E1, E2}=> |={E2, E3}=> P) ⊢ |={E1, E3}=> P
+  mask_frame_r' {E1 E2 Ef : CoPset} (P : PROP) :
+    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={CoPset.union E1 Ef, CoPset.union E2 Ef}=> P
+  frame_r {E1 E2 : CoPset} (P R : PROP) :
     iprop((|={E1, E2}=> P) ∗ R ⊢ |={E1, E2}=> P ∗ R)
 
-class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP MASK] where
-  fupd_of_bupd {P : PROP} {E : Set MASK} : iprop(⊢ |==> P) → iprop(⊢ |={E}=> P)
+class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
+  fupd_of_bupd {P : PROP} {E : CoPset} : iprop(⊢ |==> P) → iprop(⊢ |={E}=> P)
 
 class BIBUpdatePlainly (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIPlainly PROP] where
   bupd_plainly {P : PROP} : iprop((|==> ■ P)) ⊢ P
 
-class BIFUpdatePlainly (PROP MASK : Type _) [BI PROP] [BIFUpdate PROP MASK] [BIPlainly PROP] where
-  fupd_plainly_keep_l (E E' : Set MASK) (P R : PROP) : (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R
-  fupd_plainly_later (E : Set MASK) (P : PROP) : (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P
-  fupd_plainly_sForall_2 (E : Set MASK) (Φ : PROP → Prop) :
+class BIFUpdatePlainly (PROP : Type _) [BI PROP] [BIFUpdate PROP] [BIPlainly PROP] where
+  fupd_plainly_keep_l (E E' : CoPset) (P R : PROP) : (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R
+  fupd_plainly_later (E : CoPset) (P : PROP) : (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P
+  fupd_plainly_sForall_2 (E : CoPset) (Φ : PROP → Prop) :
     (∀ p, ⌜Φ p⌝ → |={E}=> ■ p) ⊢ |={E}=> sForall Φ
 
 section BUpdLaws
diff --git a/src/Iris/Std/Classes.lean b/src/Iris/Std/Classes.lean
index a2e88a81..95610287 100644
--- a/src/Iris/Std/Classes.lean
+++ b/src/Iris/Std/Classes.lean
@@ -56,4 +56,13 @@ class Antisymmetric (R : Relation α) (S : outParam <| Relation α) where
   antisymm {x y : α} : (left : S x y) → (right : S y x) → R x y
 export Antisymmetric (antisymm)
 
+class Disjoint (α : Type u) where
+  disjoint : α -> α -> Prop
+export Disjoint (disjoint)
+infix:50 " ## " => Disjoint.disjoint
+
+class Injective (f : A -> B) where
+  inj : ∀ (a a' : A), f a = f a' -> a = a'
+export Injective (inj)
+
 end Iris.Std
diff --git a/src/Iris/Std/CoPset.lean b/src/Iris/Std/CoPset.lean
new file mode 100644
index 00000000..7cce0587
--- /dev/null
+++ b/src/Iris/Std/CoPset.lean
@@ -0,0 +1,433 @@
+import Iris.Std.Positives
+import Iris.Std.Classes
+
+/- This file implements an abstract type [CoPset] of (possibly infinite) sets
+of positive binary natural numbers ([Pos]). This type supports the
+following operations:
+
+· the empty set;
+· a singleton set;
+· the full set;
+· union, intersection, and complement;
+· picking an element in an infinite set;
+· splitting a set into two disjoint subsets in such a way that if the original
+  set is infinite then both parts are infinite;
+· the (infinite) set of all numbers that have a certain suffix;
+· conversions to and from other representations of sets.
+-/
+
+/-- The raw tree data structure -/
+
+/- [coPset.leaf false] is the empty set; [coPset.leaf true] is the full set. -/
+/- In [coPset.node b l r], the Boolean flag [b] indicates whether the number
+1 is a member of the set, while the subtrees [l] and [r] must be
+consulted to determine whether a number of the form [2i] or [2i+1]
+is a member of the set. -/
+
+private inductive CoPsetRaw where
+  | leaf : Bool → CoPsetRaw
+  | node : Bool → CoPsetRaw → CoPsetRaw → CoPsetRaw
+deriving DecidableEq
+
+/-- The type of raw trees (above) offers several representations of the
+empty set and several representations of the full set. In order to
+achieve extensional equality, this redundancy must be eliminated.
+This is achieved by imposing a well-formedness criterion on trees. -/
+def coPset_wf (t : CoPsetRaw) : Bool :=
+  match t with
+  | .leaf _ => true
+  | .node true (.leaf true) (.leaf true) => false
+  | .node false (.leaf false) (.leaf false) => false
+  | .node _ l r => coPset_wf l && coPset_wf r
+
+theorem node_wf_l b l r : coPset_wf (.node b l r) -> coPset_wf l := by
+  cases b <;> rcases l with ⟨⟨⟩⟩ | _ <;> rcases r with ⟨⟨⟩⟩ | _ <;>
+  simp_all [coPset_wf]
+theorem node_wf_r b l r : coPset_wf (.node b l r) -> coPset_wf r := by
+  cases b <;> rcases l with ⟨⟨⟩⟩ | _ <;> rcases r with ⟨⟨⟩⟩ | _ <;>
+  simp_all [coPset_wf]
+
+/-- The smart constructor [node'] preserves well-formedness. -/
+def CoPsetRaw.node' (b : Bool) (l r : CoPsetRaw) : CoPsetRaw :=
+  match b, l, r with
+  | true, .leaf true, .leaf true => .leaf true
+  | false, .leaf false, .leaf false => .leaf false
+  | _, _, _ => .node b l r
+
+theorem node'_wf b l r :
+  coPset_wf l -> coPset_wf r -> coPset_wf (CoPsetRaw.node' b l r) := by
+  cases b <;> rcases l with ⟨ ⟨⟩ ⟩ | _ <;> rcases r with ⟨ ⟨⟩ ⟩ | _ <;>
+  simp [CoPsetRaw.node', coPset_wf] <;> exact fun a_6 a_7 => ⟨a_6, a_7⟩
+
+open CoPsetRaw
+
+/-- The membership test. -/
+def CoPsetRaw.ElemOf : Pos → CoPsetRaw → Bool
+  | _, leaf b => b
+  | .xH, node b _ _ => b
+  | p~0, node _ l _ => CoPsetRaw.ElemOf p l
+  | p~1, node _ _ r => CoPsetRaw.ElemOf p r
+instance : Membership Pos CoPsetRaw  where
+  mem := fun t p => CoPsetRaw.ElemOf p t
+
+theorem elem_of_node b l r (p : Pos) :
+  (CoPsetRaw.ElemOf p (CoPsetRaw.node' b l r)) = (CoPsetRaw.ElemOf p (CoPsetRaw.node b l r)) := by
+  cases p <;> cases b <;> rcases l with ⟨⟨⟩⟩ | _ <;> rcases r with ⟨⟨⟩⟩ | _ <;>
+  simp [node', CoPsetRaw.ElemOf]
+
+
+/-- Singleton. -/
+def CoPsetRaw.Singleton : Pos → CoPsetRaw
+  | .xH => node true (leaf false) (leaf false)
+  | p~0 => node' false (Singleton p) (leaf false)
+  | p~1 => node' false (leaf false) (Singleton p)
+
+/-- Union -/
+def CoPsetRaw.Union : CoPsetRaw → CoPsetRaw → CoPsetRaw
+  | leaf false, t => t
+  | t, leaf false => t
+  | leaf true, _ => leaf true
+  | _, leaf true => leaf true
+  | node b1 l1 r1, node b2 l2 r2 =>
+    node' (b1 || b2) (Union l1 l2) (Union r1 r2)
+instance : Union CoPsetRaw where union := CoPsetRaw.Union
+
+/-- Intersection -/
+def CoPsetRaw.Intersection : CoPsetRaw → CoPsetRaw → CoPsetRaw
+  | leaf true, t => t
+  | t, leaf true => t
+  | leaf false, _ => leaf false
+  | _, leaf false => leaf false
+  | node b1 l1 r1, node b2 l2 r2 =>
+    node' (b1 && b2) (Intersection l1 l2) (Intersection r1 r2)
+instance : Inter CoPsetRaw where inter := CoPsetRaw.Intersection
+
+/-- Complement -/
+def CoPsetRaw.Complement : CoPsetRaw → CoPsetRaw
+  | leaf b => leaf (!b)
+  | node b l r => node' (!b) (Complement l) (Complement r)
+
+/-- Well-formedness for the above operations -/
+
+theorem coPsetSingleton_wf p : coPset_wf (CoPsetRaw.Singleton p) := by
+  induction p <;> simp_all [CoPsetRaw.Singleton, coPset_wf]
+  · apply node'_wf; simp [coPset_wf]; assumption
+  · apply node'_wf; assumption; simp [coPset_wf]
+
+theorem coPsetUnion_wf t1 t2 :
+  coPset_wf t1 -> coPset_wf t2 -> coPset_wf (t1 ∪ t2) := by
+  revert t2; induction t1 with
+  | leaf b =>
+    intros t2 Hwf1 Hwf2; cases b <;> simp [Union.union, CoPsetRaw.Union]
+    · assumption
+    · rcases t2 with ⟨⟨⟩⟩ | _ <;> simp [CoPsetRaw.Union, coPset_wf]
+  | node b l r IH1 IH2 =>
+    intros t2 Hwf1 Hwf2; rcases t2 with ⟨⟨⟩⟩ | _ <;> simp [Union.union, CoPsetRaw.Union, coPset_wf]
+    · assumption
+    · apply node'_wf
+      · apply IH1; exact node_wf_l b l r Hwf1
+        (expose_names; exact node_wf_l a a_1 a_2 Hwf2)
+      · apply IH2; exact node_wf_r b l r Hwf1
+        (expose_names; exact node_wf_r a a_1 a_2 Hwf2)
+
+theorem coPsetIntersection_wf t1 t2 :
+  coPset_wf t1 -> coPset_wf t2 -> coPset_wf (t1 ∩ t2) := by
+  revert t2; induction t1 with
+  | leaf b =>
+    intros t2 Hwf1 Hwf2; cases b <;> simp [Inter.inter, CoPsetRaw.Intersection]
+    · rcases t2 with ⟨⟨⟩⟩ | _ <;> simp [CoPsetRaw.Intersection, coPset_wf]
+    · assumption
+  | node b l r IH1 IH2 =>
+    intros t2 Hwf1 Hwf2; rcases t2 with ⟨⟨⟩⟩ | _ <;> simp [Inter.inter, CoPsetRaw.Intersection, coPset_wf]
+    · assumption
+    · apply node'_wf
+      · apply IH1; exact node_wf_l b l r Hwf1
+        (expose_names; exact node_wf_l a a_1 a_2 Hwf2)
+      · apply IH2; exact node_wf_r b l r Hwf1
+        (expose_names; exact node_wf_r a a_1 a_2 Hwf2)
+
+theorem coPsetComplement_wf t : coPset_wf (CoPsetRaw.Complement t) := by
+  induction t with
+  | leaf b => cases b <;> simp [CoPsetRaw.Complement, coPset_wf]
+  | node b l r => cases b <;> simp [CoPsetRaw.Complement, coPset_wf] <;>
+    apply node'_wf <;> assumption
+
+/-- The abstract type [CoPset] -/
+/- A set is a well-formed tree. -/
+structure CoPset where
+  tree : CoPsetRaw
+  wf : coPset_wf tree = true
+
+instance : Membership Pos CoPset where mem E p := p ∈ E.tree
+
+namespace CoPset
+
+/-- All operations are refined at the level of [CoPset] -/
+
+def empty : CoPset := ⟨CoPsetRaw.leaf false, rfl⟩
+instance : EmptyCollection CoPset where emptyCollection := CoPset.empty
+
+def full : CoPset := ⟨CoPsetRaw.leaf true, rfl⟩
+
+def singleton (p : Pos) : CoPset :=
+  ⟨CoPsetRaw.Singleton p, coPsetSingleton_wf p⟩
+
+def union (X Y : CoPset) : CoPset :=
+  ⟨CoPsetRaw.Union X.tree Y.tree, coPsetUnion_wf _ _ X.wf Y.wf⟩
+instance : Union CoPset where union := CoPset.union
+
+def inter (X Y : CoPset) : CoPset :=
+  ⟨CoPsetRaw.Intersection X.tree Y.tree, coPsetIntersection_wf _ _ X.wf Y.wf⟩
+instance : Inter CoPset where inter := CoPset.inter
+
+def complement (X : CoPset) : CoPset :=
+  ⟨CoPsetRaw.Complement X.tree, coPsetComplement_wf _⟩
+
+def diff (X Y : CoPset) : CoPset := X ∩ (complement Y)
+
+def mem (p : Pos) (X : CoPset) : Bool :=
+  CoPsetRaw.ElemOf p X.tree
+
+instance : HasSubset CoPset where
+  Subset t1 t2 := ∀ (p : Pos), p ∈ t1 -> p ∈ t2
+
+instance : SDiff CoPset where
+  sdiff := CoPset.diff
+
+theorem in_inter p (X Y : CoPset) :
+  p ∈ X ∩ Y <-> p ∈ X ∧ p ∈ Y := by
+  simp [Inter.inter, inter, CoPsetRaw.Intersection]
+  simp [Membership.mem, ElemOf, CoPsetRaw.ElemOf]
+  constructor
+  · rcases X with ⟨X, xwf⟩; rcases Y with ⟨Y, ywf⟩; simp []
+    induction p generalizing X Y with
+    | xI p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [Intersection] <;> intros Hnin <;>
+      try simp_all [CoPsetRaw.ElemOf]
+      apply (IH _ (node_wf_r _ _ _ xwf) _ (node_wf_r _ _ _ ywf))
+      rewrite [elem_of_node] at Hnin; simp_all [ElemOf]
+    | xO p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [Intersection] <;> intros Hnin <;>
+      try simp_all [CoPsetRaw.ElemOf]
+      apply (IH _ (node_wf_l _ _ _ xwf) _ (node_wf_l _ _ _ ywf))
+      rewrite [elem_of_node] at Hnin; simp_all [ElemOf]
+    | xH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [Intersection, ElemOf, elem_of_node]
+
+  · rcases X with ⟨X, xwf⟩; rcases Y with ⟨Y, ywf⟩; simp []
+    induction p generalizing X Y with
+    | xI p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [ElemOf, elem_of_node, Intersection]
+      apply (IH _ (node_wf_r _ _ _ xwf) _ (node_wf_r _ _ _ ywf))
+    | xO p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [ElemOf, elem_of_node, Intersection]
+      apply (IH _ (node_wf_l _ _ _ xwf) _ (node_wf_l _ _ _ ywf))
+    | xH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [ElemOf, elem_of_node, Intersection]
+      exact fun a_6 a_7 => ⟨a_6, a_7⟩
+
+theorem in_complement p (X : CoPset) :
+  p ∈ complement X <-> p ∉ X := by
+  simp [complement, CoPsetRaw.Complement]
+  simp [Membership.mem, ElemOf, CoPsetRaw.ElemOf]
+  rcases X with ⟨X, xwf⟩; simp []
+  induction p generalizing X with
+    | xI p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;>
+      simp [CoPsetRaw.Complement, CoPsetRaw.ElemOf, elem_of_node]
+      apply IH; apply node_wf_r _ _ _ xwf
+    | xO p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;>
+      simp [CoPsetRaw.Complement, CoPsetRaw.ElemOf, elem_of_node]
+      apply IH; apply node_wf_l _ _ _ xwf
+    | xH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> simp [CoPsetRaw.Complement, CoPsetRaw.ElemOf, elem_of_node]
+
+theorem in_diff p (X Y : CoPset) :
+  p ∈ X \ Y <-> p ∈ X ∧ p ∉ Y := by
+  simp [SDiff.sdiff, CoPset.diff]
+  constructor
+  · intros Hnin; obtain ⟨ Hx, Hy ⟩ := (in_inter p X (complement Y)).1 Hnin
+    constructor
+    · exact Hx
+    · exact ((in_complement p Y).1 Hy)
+  · rintro ⟨ Hx, Hy ⟩
+    simp [in_inter, in_diff]
+    constructor
+    · exact Hx
+    · exact ((in_complement p Y).2 Hy)
+
+theorem in_union p (X Y : CoPset) :
+  p ∈ X ∪ Y <-> p ∈ X ∨ p ∈ Y := by
+  rcases X with ⟨X, xwf⟩; rcases Y with ⟨Y, ywf⟩
+  simp [Membership.mem, ElemOf, CoPsetRaw.ElemOf]
+  constructor
+  · induction p generalizing X Y with
+    | xI p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp_all [Union.union, union, CoPsetRaw.Union, ElemOf, elem_of_node] <;> intros Hin <;>
+      try simp_all [CoPsetRaw.ElemOf]
+      apply (IH _ (node_wf_r _ _ _ xwf) _ (node_wf_r _ _ _ ywf))
+      simp_all [ElemOf]
+    | xO p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp_all [ElemOf, Union.union, union, CoPsetRaw.Union]
+      simp_all [elem_of_node, CoPsetRaw.ElemOf]; intros Hin
+      apply (IH _ (node_wf_l _ _ _ xwf) _ (node_wf_l _ _ _ ywf))
+      simp_all [ElemOf]
+    | xH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [Union.union, union, CoPsetRaw.Union, ElemOf, elem_of_node]
+
+  · induction p generalizing X Y with
+    | xI p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp_all [Union.union, union, CoPsetRaw.Union, ElemOf, elem_of_node] <;> intros Hin <;>
+      apply (IH _ (node_wf_r _ _ _ xwf) _ (node_wf_r _ _ _ ywf) Hin)
+    | xO p IH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp_all [ElemOf, Union.union, union, CoPsetRaw.Union]
+      simp_all [elem_of_node, CoPsetRaw.ElemOf]; intros Hin
+      apply (IH _ (node_wf_l _ _ _ xwf) _ (node_wf_l _ _ _ ywf) Hin)
+    | xH =>
+      rcases X with ⟨⟨⟩⟩ | _ <;> rcases Y with ⟨⟨⟩⟩ | _ <;>
+      simp [Union.union, union, CoPsetRaw.Union, ElemOf, elem_of_node]
+
+theorem not_in_union p (X1 X2 : CoPset) :
+  ¬ p ∈ X1 ∪ X2 <-> ¬ p ∈ X1 ∧ ¬ p ∈ X2 := by
+  constructor
+  · intros Hunion; constructor <;> intro Hnin <;>
+    apply Hunion <;> simp [in_union]
+    · left; assumption
+    · right; assumption
+  · rintro ⟨ Hnin1, Hnin2 ⟩; intro Hunion; simp [in_union] at Hunion
+    cases Hunion
+    · apply Hnin1; assumption
+    · apply Hnin2; assumption
+
+theorem subseteq_trans (X Y Z : CoPset) :
+  X ⊆ Y ->
+  Y ⊆ Z ->
+  X ⊆ Z := by
+  intros Hxy Hyz p Hx
+  exact Hyz p (Hxy p Hx)
+
+def CoPsetRaw.isFinite : CoPsetRaw → Bool
+  | CoPsetRaw.leaf b => !b
+  | CoPsetRaw.node _ l r => isFinite l && isFinite r
+
+def isFinite (X : CoPset) : Bool :=
+  CoPsetRaw.isFinite X.tree
+
+/-- Picking an element out of an infinite set -/
+
+/- Provided that the set [X] is infinite, [pick X] yields an element of
+this set. Note that [pick] is implemented by depth-first search, so
+using it repeatedly to obtain elements [x] and inserting these elements
+[x] into some set [Y] will give rise to a very unbalanced tree. -/
+
+def CoPsetRaw.pickRaw : CoPsetRaw → Option Pos
+  | CoPsetRaw.leaf true => some Pos.P1
+  | CoPsetRaw.node true _ _ => some Pos.P1
+  | CoPsetRaw.leaf false => none
+  | CoPsetRaw.node false l r =>
+    match pickRaw l with
+    | some i => some (i~0)
+    | none => Option.map (λ i => i~1) (pickRaw r)
+
+def CoPset.pick (X : CoPset) : Pos :=
+  (CoPsetRaw.pickRaw X.tree).getD Pos.P1
+
+
+-- Inverse suffix closure
+
+/-- [suffixes q] is the set of all numbers [p] such that [q] is a suffix
+of [p], when these numbers are viewed as sequences of bits. In other words, it
+is the set of all numbers that have the suffix [q]. It is always an infinite
+set. -/
+def CoPsetRaw.suffixesRaw : Pos → CoPsetRaw
+  | .xH => .leaf true
+  | p~0 => CoPsetRaw.node' false (suffixesRaw p) (.leaf false)
+  | p~1 => CoPsetRaw.node' false (.leaf false) (suffixesRaw p)
+
+theorem coPsetSuffixes_wf p : coPset_wf (CoPsetRaw.suffixesRaw p) := by
+  induction p <;> simp [CoPsetRaw.suffixesRaw, coPset_wf] <;>
+  apply node'_wf <;> simp_all [coPset_wf]
+
+def suffixes (p : Pos) : CoPset :=
+  ⟨CoPsetRaw.suffixesRaw p, coPsetSuffixes_wf p⟩
+theorem elem_suffixes p q : p ∈ suffixes q <-> ∃ q', p = q' ++ q := by
+  constructor
+  · induction q generalizing p with
+    | xI q IH =>
+      simp [suffixes, CoPsetRaw.suffixesRaw]
+      simp_all [Membership.mem]; rewrite [elem_of_node]
+      intros Hin; cases p <;> simp [CoPsetRaw.ElemOf] at Hin
+      obtain ⟨ q', Heq ⟩ := (IH _ Hin)
+      exists q'; rewrite [Heq]; simp [HAppend.hAppend, Pos.app]
+    | xO q IH =>
+      simp [suffixes, CoPsetRaw.suffixesRaw]
+      simp_all [Membership.mem]; rewrite [elem_of_node]
+      intros Hin; cases p <;> simp [CoPsetRaw.ElemOf] at Hin
+      obtain ⟨ q', Heq ⟩ := (IH _ Hin)
+      exists q'; rewrite [Heq]; simp [HAppend.hAppend, Pos.app]
+    | xH =>
+      simp [suffixes, CoPsetRaw.suffixesRaw]
+      simp [Membership.mem, CoPsetRaw.ElemOf]
+      simp [HAppend.hAppend, Pos.app]
+  · intros Heq; rcases Heq with ⟨ q', Heq ⟩; rewrite [Heq]
+    simp [suffixes, Membership.mem]
+    induction q generalizing p <;> simp [CoPsetRaw.suffixesRaw] <;> try rewrite [elem_of_node] <;>
+    simp_all [HAppend.hAppend, Pos.app, CoPsetRaw.ElemOf]
+    cases q' <;> simp [CoPsetRaw.ElemOf]
+
+/-- Splitting a set -/
+
+/- Every infinite [X : CoPset] can be split into two disjoint parts, which are
+infinite sets. Use the functions [splitLeft] and [splitRight] if you
+need a constructive witness. -/
+
+def l_raw : CoPsetRaw → CoPsetRaw
+  | CoPsetRaw.leaf false => CoPsetRaw.leaf false
+  | CoPsetRaw.leaf true => CoPsetRaw.node true (CoPsetRaw.leaf true) (CoPsetRaw.leaf false)
+  | CoPsetRaw.node b l r => CoPsetRaw.node' b (l_raw l) (l_raw r)
+
+def r_raw : CoPsetRaw → CoPsetRaw
+  | CoPsetRaw.leaf false => CoPsetRaw.leaf false
+  | CoPsetRaw.leaf true => CoPsetRaw.node false (CoPsetRaw.leaf false) (CoPsetRaw.leaf true)
+  | CoPsetRaw.node _ l r => CoPsetRaw.node' false (r_raw l) (r_raw r)
+
+theorem l_wf t : coPset_wf (l_raw t) := by
+  induction t with
+  | leaf b => cases b <;> simp [l_raw, coPset_wf]
+  | node b l r => simp [l_raw]; apply node'_wf <;> assumption
+
+theorem r_wf t : coPset_wf (r_raw t) := by
+  induction t with
+  | leaf b => cases b <;> simp [r_raw, coPset_wf]
+  | node b l r => simp [r_raw]; apply node'_wf <;> assumption
+
+def splitLeft (X : CoPset) : CoPset :=
+  ⟨l_raw X.tree, l_wf _⟩
+
+def splitRight (X : CoPset) : CoPset :=
+  ⟨r_raw X.tree, r_wf _⟩
+
+def split (X : CoPset) : CoPset × CoPset :=
+  (splitLeft X, splitRight X)
+
+end CoPset
+
+instance : Iris.Std.Disjoint CoPset where
+  disjoint s t := ∀ p, p ∈ s -> p ∈ t -> False
+
+@[symm]
+theorem disj_symm (E1 E2 : CoPset) :
+  E1 ## E2 -> E2 ## E1 := by
+  exact fun Hdisj p HE1 HE2 => Hdisj p HE2 HE1
diff --git a/src/Iris/Std/Namespaces.lean b/src/Iris/Std/Namespaces.lean
new file mode 100644
index 00000000..46136ad8
--- /dev/null
+++ b/src/Iris/Std/Namespaces.lean
@@ -0,0 +1,74 @@
+import Iris.Std.CoPset
+import Iris.Std.Positives
+
+abbrev Namespace := List Pos
+
+instance : DecidableEq Namespace := by infer_instance
+instance : Pos.Countable Namespace := by infer_instance
+
+def nroot : Namespace := List.nil
+
+def ndot [Pos.Countable A] (N : Namespace) (x : A) : Namespace :=
+  (Pos.Countable.encode x) :: N
+
+def nclose (N : Namespace) : CoPset :=
+  CoPset.suffixes ((Pos.flatten N))
+
+instance : CoeOut Namespace CoPset where coe := nclose
+
+infix:80 ".@" => ndot
+
+instance ndisjoint : Iris.Std.Disjoint Namespace where
+  disjoint N1 N2 := nclose N1 ## nclose N2
+
+theorem nclose_root : ↑nroot = CoPset.full := by rfl
+
+theorem nclose_subseteq [Pos.Countable A] N (x : A) : (↑N.@x : CoPset) ⊆ (↑N : CoPset) := by
+  intros p
+  simp [nclose, ndot]
+  rewrite [CoPset.elem_suffixes]; rewrite [CoPset.elem_suffixes]
+  rintro ⟨ q, Heq ⟩; rewrite [Heq]
+  obtain ⟨ q', Heq ⟩ :=
+    (Pos.flatten_suffix N (ndot N x) (by exists [Pos.Countable.encode x]))
+  exists (q ++ q')
+  rewrite [Pos.app_assoc_l.assoc, <- Heq]
+  rfl
+
+theorem nclose_subseteq' [Pos.Countable A] E (N : Namespace) (x : A) : (↑N : CoPset) ⊆ E -> (↑(N.@x) : CoPset) ⊆ E := by
+  intro Hsubset
+  apply CoPset.subseteq_trans
+  apply nclose_subseteq
+  assumption
+
+theorem ndot_ne_disjoint [Pos.Countable A] (N : Namespace) (x y : A) :
+  x ≠ y -> N.@x ## N.@y := by
+  intros Hxy p; simp [nclose];
+  rewrite [CoPset.elem_suffixes]; rewrite [CoPset.elem_suffixes]
+  rintro ⟨ qx, Heqx ⟩; rintro ⟨ qy, Heqy ⟩
+  rewrite [Heqx] at Heqy
+  have := Pos.flatten_suffix_eq qx qy (N.@x) (N.@y) (by simp [ndot, List.length]) Heqy
+  simp [ndot, Pos.Countable.encode] at this
+  have := (Pos.encode_inj.inj _ _ this)
+  exact Hxy this
+
+theorem ndot_preserve_disjoint_l [Pos.Countable A] (N : Namespace) (E : CoPset) (x : A) :
+  ↑N ## E → ↑(N.@x) ## E := by
+  have := nclose_subseteq N x
+  simp [Iris.Std.disjoint]; simp [Subset] at this
+  intros Hdisj p; exact fun a_1 => Hdisj p (this p a_1)
+
+theorem ndot_preserve_disjoint_r [Pos.Countable A] (N : Namespace) (E : CoPset) (x : A) :
+  E ## ↑N → E ## ↑(N.@x) := by
+  intros
+  symm
+  apply ndot_preserve_disjoint_l
+  symm; assumption
+
+theorem CoPset.difference_difference (X1 X2 X3 Y : CoPset) :
+  (X1 \ X2) \ X3 ## Y -> X1 \ (X2 ∪ X3) ## Y := by
+  -- Long term, this should be solvable with one automatic tactic
+  intros Hdisj p Hnin Hin
+  apply (Hdisj p _ Hin)
+  obtain ⟨ HX1, HXU ⟩ := (in_diff p X1 (X2 ∪ X3)).1 Hnin
+  obtain ⟨ HX2, HX3 ⟩ := (not_in_union p X2 X3).1 HXU
+  simp [in_diff]; simp [*]
diff --git a/src/Iris/Std/Positives.lean b/src/Iris/Std/Positives.lean
new file mode 100644
index 00000000..04fb6768
--- /dev/null
+++ b/src/Iris/Std/Positives.lean
@@ -0,0 +1,402 @@
+import Iris.Std.Classes
+/-- [Pos] is a datatype representing the strictly positive integers
+   in a binary way. Starting from 1 (represented by [xH]), one can
+   add a new least significant digit via [xO] (digit 0) or [xI] (digit 1). -/
+
+inductive Pos where
+| xI : Pos -> Pos
+| xO : Pos -> Pos
+| xH : Pos
+deriving Repr, DecidableEq
+
+namespace Pos
+
+/- Postfix notation for positive numbers, which allows mimicking
+    the position of bits in a big-endian representation.
+    For instance, we can write [P1~1~0] instead of [(xO (xI xH))]
+    for the number 6 (which is 110 in binary notation). -/
+
+abbrev P1 : Pos := xH
+syntax term "~1" : term
+syntax term "~0" : term
+
+macro_rules
+  | `($p ~1) => `(xI $p)
+  | `($p ~0) => `(xO $p)
+
+@[app_unexpander xI]
+def unexpand_Pos_xI : Lean.PrettyPrinter.Unexpander
+  | `($_ $p) => `($p~1)
+  | _ => throw ()
+
+@[app_unexpander xO]
+def unexpand_Pos_x0 : Lean.PrettyPrinter.Unexpander
+  | `($_ $p) => `($p~0)
+  | _ => throw ()
+
+-- Operations over positive numbers
+
+/-- Successor -/
+def succ : Pos → Pos
+  | p~1     => (succ p)~0
+  | p~0   => p~1
+  | P1   => P1~0
+
+mutual
+/-- Addition -/
+def add x y :=
+  match x, y with
+    | p~1, q~1 => (add_carry p q)~0
+    | p~1, q~0 => (add p q)~1
+    | p~1, xH => (succ p)~0
+    | p~0, q~1 => (add p q)~1
+    | p~0, q~0 => (add p q)~0
+    | p~0, xH => p~1
+    | xH, q~1 => (succ q)~0
+    | xH, q~0 => q~1
+    | xH, xH => P1~0
+
+def add_carry x y :=
+  match x, y with
+    | p~1, q~1 => (add_carry p q)~1
+    | p~1, q~0 => (add_carry p q)~0
+    | p~1, xH => (succ p)~1
+    | p~0, q~1 => (add_carry p q)~0
+    | p~0, q~0 => (add p q)~1
+    | p~0, xH => (succ p)~0
+    | xH, q~1 => (succ q)~1
+    | xH, q~0 => (succ q)~0
+    | xH, xH => P1~1
+end
+
+instance : Add Pos where add := Pos.add
+
+/-- Multiplication -/
+def mul : Pos → Pos → Pos
+  | xH,     q       => q
+  | p~0,   q       => xO (mul p q)
+  | p~1,   q       => add (xO (mul p q)) q
+
+instance : Mul Pos where mul := Pos.mul
+
+
+/-- Coercions to and from Nat -/
+
+def toNat : Pos → Nat
+  | xH     => 1
+  | xO p   => 2 * p.toNat
+  | xI p   => 2 * p.toNat + 1
+
+instance : CoeOut Pos Nat where coe := Pos.toNat
+
+def compare (a b : Pos) : Ordering :=
+  Ord.compare (a.toNat) (b.toNat)
+
+/- 0%nat gets mapped to 1%pos. -/
+def ofNat (n : Nat) : Pos :=
+match n with
+| 0 => P1
+| 1 => P1
+| (n + 1) => succ (ofNat n)
+
+instance : OfNat Pos n where ofNat := Pos.ofNat n
+
+
+/- Since [Pos] represents lists of bits, we define list operations
+  on it. These operations are in reverse, as positives are treated as snoc
+  lists instead of cons lists. -/
+def app (p1 p2 : Pos) : Pos :=
+  match p2 with
+  | xH => p1
+  | p2~0 => (app p1 p2)~0
+  | p2~1 => (app p1 p2)~1
+
+@[reducible]
+instance : HAppend Pos Pos Pos where hAppend := Pos.app
+
+instance app_assoc_l : @Std.Associative Pos (.++.) where
+  assoc _ _ p := by induction p <;> simp_all [HAppend.hAppend, app]
+
+@[simp]
+theorem app_1_left_id (p : Pos) : app P1 p = p := by
+  induction p <;> simp [HAppend.hAppend, app] <;> assumption
+
+instance app_1_l : @Std.LawfulLeftIdentity Pos Pos (app) P1 where
+  left_id p := app_1_left_id p
+
+def reverse_go (p1 p2 : Pos) : Pos :=
+  match p2 with
+  | xH => p1
+  | p2~0 => reverse_go (p1~0) p2
+  | p2~1 => reverse_go (p1~1) p2
+def reverse : Pos → Pos := reverse_go P1
+
+theorem reverse_go_app (p1 p2 p3 : Pos) :
+  reverse_go p1 (p2 ++ p3) = reverse_go p1 p3 ++ reverse_go P1 p2 := by
+  have helper : ∀ p1 p2 p3, reverse_go (p2 ++ p3) p1 = p2 ++ (reverse_go p3 p1) := by
+    intro p1
+    induction p1 with
+    | xI p1 IH =>
+      intro p2 p3
+      apply (IH _ (_~1))
+    | xO p1 IH =>
+      intro p2 p3
+      apply (IH _ (_~0))
+    | xH =>
+      intro p2 p3; rfl
+
+  induction p3 generalizing p1 p2 with
+  | xI p3 IH =>
+    simp [reverse_go, HAppend.hAppend, app]
+    exact IH (p1~1) p2
+  | xO p3 IH =>
+    simp [reverse_go, HAppend.hAppend, app]
+    exact IH (p1~0) p2
+  | xH =>
+    simp [reverse_go]
+    rewrite [<- helper]
+    simp [HAppend.hAppend, app]
+
+theorem reverse_app (p1 p2 : Pos) :
+  reverse (p1 ++ p2) = reverse p2 ++ reverse p1 := by
+  simp [reverse]; apply reverse_go_app
+theorem reverse_x0 p : reverse (p~0) = (P1~0) ++ reverse p := by
+  apply (reverse_app p (P1~0))
+theorem reverse_xI p : reverse (p~1) = (P1~1) ++ reverse p := by
+  apply (reverse_app p (P1~1))
+
+/-- Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
+      1~1~0~0 -> 1~1~1~0~0~0~0 -/
+def dup  : Pos -> Pos
+| xH => P1
+| p~0 => (dup p)~0~0
+| p~1 => (dup p)~1~1
+
+
+/-- These next functions allow to efficiently encode lists of positives (bit
+strings) into a single positive and go in the other direction as well. This is
+for example used for the countable instance of lists and in namespaces.
+The main functions are [flatten] and [unflatten]. -/
+
+def flatten_go (xs : List Pos) (acc : Pos) : Pos :=
+  match xs with
+  | [] => acc
+  | x :: xs => flatten_go xs (acc~1~0 ++ reverse (dup x))
+
+/-- Flatten a list of positives into a single positive by duplicating the bits
+of each element, so that:
+
+- [0 -> 00]
+- [1 -> 11]
+
+and then separating each element with [10]. -/
+def flatten (xs : List Pos) : Pos :=
+  flatten_go xs P1
+
+def unflatten_go
+        (p : Pos)
+        (acc_xs : List Pos)
+        (acc_elm : Pos)
+  : Option (List Pos) :=
+  match p with
+  | xH => some acc_xs
+  | p'~0~0 => unflatten_go p' acc_xs (acc_elm~0)
+  | p'~1~1 => unflatten_go p' acc_xs (acc_elm~1)
+  | p'~1~0 => unflatten_go p' (acc_elm :: acc_xs) P1
+  | _ => none
+
+/-- Unflatten a positive into a list of positives, assuming the encoding
+used by [flatten]. -/
+def unflatten (p : Pos) : Option (List Pos) :=
+  unflatten_go p [] P1
+
+theorem flatten_go_app xs acc :
+    flatten_go xs acc = acc ++ flatten_go xs P1 := by
+  induction xs generalizing acc with
+  | nil => rfl
+  | cons x xs IH =>
+    simp [flatten_go]
+    rewrite [IH]
+    rewrite [IH (P1~1~0 ++ x.dup.reverse)]
+    simp only [<- app_assoc_l.assoc]
+    simp [HAppend.hAppend, app]
+
+theorem unflatten_go_app (p : Pos) suffix xs acc :
+  unflatten_go (suffix ++ reverse (dup p)) xs acc =
+  unflatten_go suffix xs (acc ++ p) := by
+  induction p generalizing suffix acc with
+  | xI p IH =>
+    simp [dup]
+    rewrite [reverse_xI]; rewrite [reverse_xI]
+    simp only [<- app_assoc_l.assoc]
+    rewrite [IH]
+    rfl
+  | xO p IH =>
+    simp [dup]
+    rewrite [reverse_x0]; rewrite [reverse_x0]
+    simp only [<- app_assoc_l.assoc]
+    rewrite [IH]
+    rfl
+  | xH => rfl
+
+theorem unflatten_flatten_go suffix xs acc :
+  unflatten_go (suffix ++ flatten_go xs P1) acc P1 =
+  unflatten_go suffix (xs ++ acc) P1 := by
+  revert suffix acc
+  induction xs with
+  | nil => intros suff acc; rfl
+  | cons x xs IH =>
+    simp [flatten_go]
+    intros suff acc
+    rewrite [flatten_go_app]
+    rewrite [<- app_assoc_l.assoc]
+    rewrite [IH]
+    rewrite [<- app_assoc_l.assoc]
+    rewrite [unflatten_go_app]
+    simp [HAppend.hAppend, app]
+    rfl
+
+theorem unflatten_flatten xs :
+  unflatten (flatten xs) = some xs := by
+  unfold flatten; unfold unflatten
+  rewrite [<- (app_1_l.left_id (flatten_go xs P1))]
+  have := unflatten_flatten_go P1 xs []
+  simp [HAppend.hAppend] at this
+  simp [this, Append.append]
+  rfl
+
+theorem flatten_app xs ys :
+  flatten (xs ++ ys) = flatten xs ++ flatten ys := by
+  unfold flatten
+  induction xs generalizing ys with
+  | nil =>
+    simp [flatten_go, HAppend.hAppend]; rfl
+  | cons x xs IH =>
+    simp [flatten_go]
+    rewrite [flatten_go_app]; rewrite [flatten_go_app xs]
+    rewrite [IH]
+    simp [app_assoc_l.assoc]
+
+theorem flatten_cons x xs :
+  flatten (x :: xs)
+  = P1~1~0 ++ reverse (dup x) ++ flatten xs := by
+  have heq : x :: xs = [x] ++ xs := rfl
+  rw [heq]
+  apply flatten_app
+
+theorem flatten_suffix (l k : List Pos) :
+  l <:+ k -> ∃ q, flatten k = q ++ flatten l := by
+  rintro ⟨ l', Heq ⟩; rewrite [<- Heq]
+  exists (flatten l')
+  apply flatten_app
+
+instance app_inj (p : Pos) : Iris.Std.Injective (.++ p) where
+  inj := by
+    intros a a' Heq
+    induction p <;> simp_all [HAppend.hAppend, app]
+
+theorem reverse_involutive p : reverse (reverse p) = p := by
+  induction p with
+  | xI p IH =>
+    rewrite [reverse_xI, reverse_app, IH]; rfl
+  | xO p IH =>
+    rewrite [reverse_x0, reverse_app, IH]; rfl
+  | xH => rfl
+
+instance rev_inj : Iris.Std.Injective reverse where
+  inj := by
+    intros p q Heq
+    rewrite [<- reverse_involutive p]
+    rewrite [<- reverse_involutive q]
+    simp [Heq]
+
+theorem dup_app p q : dup (p ++ q) = dup p ++ dup q := by
+  induction q generalizing p <;>
+  simp_all [HAppend.hAppend, app, dup]
+
+theorem reverse_dup (p : Pos) :
+  reverse (dup p) = dup (reverse p) := by
+  have hdup := dup_app
+  have hassoc := app_assoc_l.assoc
+  simp [HAppend.hAppend, app] at hdup hassoc
+  induction p with
+  | xI p IH =>
+    simp [dup]
+    simp [reverse_xI, HAppend.hAppend, app]
+    rewrite [<- hassoc, IH, hdup]
+    rfl
+  | xO p IH =>
+    simp [dup]
+    simp [reverse_x0, HAppend.hAppend, app]
+    rewrite [<- hassoc, IH, hdup]
+    rfl
+  | xH => rfl
+
+theorem dup_suffix_eq p q s1 s2 :
+  s1~1~0 ++ dup p = s2~1~0 ++ dup q -> p = q := by
+  induction p generalizing q with
+  | xI p IH =>
+    intros Heq
+    cases q <;> simp_all [HAppend.hAppend, app, dup] <;> rename Pos => q
+    rewrite [IH q]; rfl; simp [Heq]
+  | xO p IH =>
+    intros Heq
+    cases q <;> simp_all [HAppend.hAppend, app, dup] <;> rename Pos => q
+    rewrite [IH q]; rfl; simp [Heq]
+  | xH => cases q <;> simp [HAppend.hAppend, app, dup]
+
+theorem flatten_suffix_eq p1 p2 (xs ys : List Pos) :
+  List.length xs = List.length ys ->
+  p1 ++ flatten xs = p2 ++ flatten ys ->
+  xs = ys := by
+  induction xs generalizing p1 p2 ys with
+  | nil => simp; intros Hlen _; apply List.eq_nil_of_length_eq_zero; symm; assumption
+  | cons x xs IH =>
+    rcases ys with _ | ⟨ y, ys ⟩; intros Hlen _; simp [List.length] at Hlen;
+    rewrite [flatten_cons]
+    rewrite [<- app_assoc_l.assoc]; rewrite [<- app_assoc_l.assoc]
+    rewrite [flatten_cons]
+    rewrite [<- app_assoc_l.assoc]; rewrite [<- app_assoc_l.assoc]
+    intros Hlen Hl
+    have Heq : xs = ys := by apply IH; simp_all []; apply Hl
+    rewrite [Heq]; congr; rewrite [Heq] at Hl
+    replace Hl := (app_inj (flatten ys)).inj _ _ Hl
+    rewrite [reverse_dup] at Hl
+    rewrite [reverse_dup] at Hl
+    replace Hl := (dup_suffix_eq _ _ p1 p2 Hl)
+    apply (rev_inj.inj _ _ Hl)
+
+
+class Countable (A : Type) where
+  encode : A -> Pos
+  decode : Pos -> Option A
+  decode_encode x : decode (encode x) = some x
+
+instance some_inj {A} : Iris.Std.Injective (@some A) where
+  inj := by intros x y; rintro ⟨⟩; rfl
+
+instance encode_inj [c : Countable A] : Iris.Std.Injective (c.encode) where
+  inj := by
+    intros x y Hxy; apply some_inj.inj
+    rewrite [<- c.decode_encode x, Hxy, c.decode_encode]
+    rfl
+
+instance [Countable A] : Countable (List A) where
+  encode xs := Pos.flatten (List.map Countable.encode xs)
+  decode p := do
+    let positives ← (Pos.unflatten p);
+    List.mapM Countable.decode positives
+  decode_encode := by
+    intros xs
+    rewrite [Pos.unflatten_flatten]; simp
+    induction xs with
+    | nil => rfl
+    | cons x xs IH =>
+      simp [List.map]; rewrite [IH]; rewrite [Countable.decode_encode]; simp
+
+instance : Countable Pos where
+  encode := id
+  decode := some
+  decode_encode _ := rfl
+
+end Pos