From 93aae7e34e7130d9541d3441079448f156d93477 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 6 Apr 2023 16:57:25 +0100
Subject: Migrate Env to use Thinned.

---
 src/Core/Term.idr | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/Core/Term.idr')

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index e52545d..182e1ea 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -81,3 +81,11 @@ expandShift :
   (thin : sx `Thins` sy) ->
   expand (shift t thin) = wkn (expand t) thin
 expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin
+
+export
+shiftHomo :
+  (t : Thinned sx) ->
+  (thin1 : sx `Thins` sy) ->
+  (thin2 : sy `Thins` sz) ->
+  shift (shift t thin1) thin2 = shift t (thin2 . thin1)
+shiftHomo (term `Over` thin) thin1 thin2 = cong (term `Over`) $ compAssoc thin2 thin1 thin
-- 
cgit v1.2.3