From 69d8b5c52f8685e3b6332b1fa9892d2f1060adc4 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 16 Apr 2023 15:25:29 +0100
Subject: Prove weakening a thinned term is homomorphic.

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

diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr
index 3ed4779..3a06612 100644
--- a/src/Core/Term/Thinned.idr
+++ b/src/Core/Term/Thinned.idr
@@ -47,3 +47,11 @@ wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $
   ~~ wkn (wkn t thin1) thin ...(sym $ wknHomo t thin1 thin)
   ~~ wkn (wkn u thin2) thin ...(cong (flip wkn thin) prf)
   ~~ wkn u (thin . thin2)   ...(wknHomo u thin2 thin)
+
+export
+wknHomo :
+  (t : Thinned k) ->
+  (thin1 : k `Thins` m) ->
+  (thin2 : m `Thins` n) ->
+  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
+wknHomo (t `Over` thin) thin1 thin2 = cong (t `Over`) (compAssoc thin2 thin1 thin)
-- 
cgit v1.2.3