diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
index 662c405dff..0671c14a03 100644
--- a/src/Codata/Musical/Colist.agda
+++ b/src/Codata/Musical/Colist.agda
@@ -18,8 +18,7 @@ open import Data.Bool.Base using (Bool; true; false)
 open import Data.Empty using (⊥)
 open import Data.Maybe using (Maybe; nothing; just; Is-just)
 open import Data.Maybe.Relation.Unary.Any using (just)
-open import Data.Nat.Base using (ℕ; zero; suc; _≥′_; ≤′-refl; ≤′-step)
-open import Data.Nat.Properties using (s≤′s)
+open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty using (List⁺; _∷_)
 open import Data.Product as Prod using (∃; _×_; _,_)