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 ¡