diff --git a/_CoqProject b/_CoqProject
index 53a3c0def87690092e9eabc775cf6a11b59fdd07..118a945f6adcf71cd1ba81e980399485d6112af5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,6 +55,7 @@ algebra/upred_tactics.v
 algebra/upred_big_op.v
 algebra/upred_hlist.v
 algebra/frac.v
+algebra/count.v
 algebra/csum.v
 algebra/list.v
 algebra/updates.v
diff --git a/algebra/count.v b/algebra/count.v
new file mode 100644
index 0000000000000000000000000000000000000000..b9ae12650218e70a7f930cf8c3b275f8c7a67204
--- /dev/null
+++ b/algebra/count.v
@@ -0,0 +1,21 @@
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import upred.
+Notation count := nat (only parsing).
+
+Section count.
+Canonical Structure countC := leibnizC count.
+
+Instance count_valid : Valid count := λ _, True.
+Instance count_pcore : PCore count := λ _, None.
+Instance count_op : Op count := λ x y, (x + y)%nat.
+
+Definition count_ra_mixin : RAMixin nat.
+Proof. by split; try apply _. Qed.
+Canonical Structure countR := discreteR count count_ra_mixin.
+End count.
+
+(** Internalized properties *)
+Lemma count_equivI {M} (x y : count) : x ≡ y ⊣⊢ (x = y : uPred M).
+Proof. by uPred.unseal. Qed.
+Lemma count_validI {M} (x : count) : ✓ x ⊣⊢ (True : uPred M).
+Proof. by uPred.unseal. Qed.
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 62bb4a4c689b71ec3bcf25f3bd0016410e299e0a..d184fa8fdc0d4d2432f1f888d739e3a0ecbf8712 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -34,7 +34,7 @@ Proof.
 Qed.
 
 (** A typeclass for whether a variable is bound in a given
-   context. Making this a typeclass means we can use tpeclass search
+   context. Making this a typeclass means we can use typeclass search
    to program solving these constraints, so this becomes extensible.
    Also, since typeclass search runs *after* unification, Coq has already
    inferred the X for us; if we were to go for embedded proof terms ot