From d5f8497dbb6de72d9664f48d6acbc9772de77be3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 1 Jun 2023 17:07:41 +0100
Subject: Give a logical relation template.

---
 src/Thinning.idr | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/Thinning.idr')

diff --git a/src/Thinning.idr b/src/Thinning.idr
index 0e99711..a79f0f5 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -142,3 +142,12 @@ keepHomo (Drop thin2) (Keep thin1) = Refl
 keepHomo (Keep thin2) Id = Refl
 keepHomo (Keep thin2) (Drop thin) = Refl
 keepHomo (Keep thin2) (Keep thin) = Refl
+
+export
+keepDrop :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  keep thin2 . Drop thin1 = Drop (thin2 . thin1)
+keepDrop Id thin1 = Refl
+keepDrop (Drop thin2) thin1 = Refl
+keepDrop (Keep thin2) thin1 = Refl
-- 
cgit v1.2.3