From 19141b121b350faf81c56f48e9fc1f0946f4a77d Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 20 Jun 2024 09:29:49 +0200
Subject: [PATCH] Add thinning from empty list

---
 src/Thinning.agda | 6 ++++++
 1 file changed, 6 insertions(+)

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 ¡