diff --git a/src/Thinning.agda b/src/Thinning.agda
index ffed3d7..05440f4 100644
--- a/src/Thinning.agda
+++ b/src/Thinning.agda
@@ -45,3 +45,9 @@ end ∘ end = end
 include α ∘ include β = include (α ∘ β)
 include α ∘ exclude β = exclude (α ∘ β)
 exclude α ∘ β = exclude (α ∘ β)
+
+-- There is always a Thinning from the empty list to any list. Here we exclude
+-- at every step.
+¡ : Thinning A [] xs
+¡ {xs = []} = end
+¡ {xs = x ∷ xs} = exclude ¡