diff --git a/_CoqProject b/_CoqProject
index 118a945f6adcf71cd1ba81e980399485d6112af5..53a3c0def87690092e9eabc775cf6a11b59fdd07 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,7 +55,6 @@ 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
deleted file mode 100644
index b9ae12650218e70a7f930cf8c3b275f8c7a67204..0000000000000000000000000000000000000000
--- a/algebra/count.v
+++ /dev/null
@@ -1,21 +0,0 @@
-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.