Prove some (non-)identity properties.

1 files changed, 15 insertions, 0 deletions

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