From ea4c4a98486f57f09d634318676cca84f3046568 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 7 Apr 2023 17:50:13 +0100
Subject: Prove some (non-)identity properties.

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

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index a41536e..f54d9e9 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -43,6 +43,21 @@ public export
 wkn1 : (0 sx : Context) -> (0 n : Name) -> sx `Thins` sx :< n
 wkn1 sx n = drop (id sx) n
 
+-- Properties
+
+export
+dropIsNotId : (thin : sx `Thins` sy) -> (0 n : Name) -> IsNotId (drop thin n)
+dropIsNotId IsId n = ItIsThinner
+dropIsNotId (IsThinner thinner) n = ItIsThinner
+
+export
+keepIdIsId : (0 sx : Context) -> (0 n : Name) -> keep (id sx) n = id (sx :< n)
+keepIdIsId sx n = Refl
+
+export
+keepNotIdIsNotId : IsNotId thin -> (0 n : Name) -> IsNotId (keep thin n)
+keepNotIdIsNotId ItIsThinner n = ItIsThinner
+
 -- Views -----------------------------------------------------------------------
 
 public export
-- 
cgit v1.2.3