diff --git a/src/Thinning/Properties.agda b/src/Thinning/Properties.agda
index a77a20a..6559fc8 100644
--- a/src/Thinning/Properties.agda
+++ b/src/Thinning/Properties.agda
@@ -2,7 +2,7 @@
 
 module Thinning.Properties where
 
-open import Data.List.Base using (List)
+open import Data.List.Base using (List; [])
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
@@ -48,3 +48,8 @@ assoc (exclude θ) (include φ) (include ψ) = cong exclude (assoc θ φ ψ)
 assoc (exclude θ) (include φ) (exclude ψ) = cong exclude (assoc (exclude θ) (include φ) ψ)
 assoc (exclude θ) (exclude φ) (include ψ) = cong exclude (assoc (exclude θ) φ ψ)
 assoc (exclude θ) (exclude φ) (exclude ψ) = cong exclude (assoc (exclude θ) (exclude φ) ψ)
+
+-- ¡ is the only Thinning from []
+¡-unique : (θ : Thinning A [] xs) → ¡ ≡ θ
+¡-unique end = refl
+¡-unique (exclude θ) = cong exclude (¡-unique θ)