Prove weakening of type judgements.

This is a huge commit that has many more changes. I should split
this up later.

1 files changed, 21 insertions, 0 deletions

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index 74ef7af..a3ddac5 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -4,6 +4,8 @@ import Core.Thinning
 
 import public Data.Fin
 
+import Syntax.PreorderReasoning
+
 -- Definition ------------------------------------------------------------------
 
 public export
@@ -29,6 +31,14 @@ wkn (Abs t) thin = Abs (wkn t $ keep thin)
 wkn (App t u) thin = App (wkn t thin) (wkn u thin)
 
 export
+wknId : (t : Term n) -> wkn t (id n) = t
+wknId (Var i) = cong Var (wknId i)
+wknId Set = Refl
+wknId (Pi t u) = cong2 Pi (wknId t) (trans (cong (wkn u) $ keepIdIsId n) (wknId u))
+wknId (Abs t) = cong Abs (trans (cong (wkn t) $ keepIdIsId n) (wknId t))
+wknId (App t u) = cong2 App (wknId t) (wknId u)
+
+export
 wknHomo :
   (t : Term k) ->
   (thin1 : k `Thins` m) ->
@@ -48,3 +58,14 @@ wknHomo (Abs t) thin1 thin2 =
       (wknHomo t (keep thin1) (keep thin2))
       (cong (wkn t) $ compKeep thin2 thin1))
 wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
+
+export
+wkn1Comm :
+  (t : Term m) ->
+  (thin : m `Thins` n) ->
+  wkn (wkn t thin) (wkn1 n) = wkn (wkn t $ wkn1 m) (keep thin)
+wkn1Comm t thin = Calc $
+  |~ wkn (wkn t thin) (wkn1 n)
+  ~~ wkn t (wkn1 n . thin)            ...(wknHomo t thin (wkn1 n))
+  ~~ wkn t (keep thin . wkn1 m)       ...(sym $ cong (wkn t) $ wkn1Comm thin)
+  ~~ wkn (wkn t $ wkn1 m) (keep thin) ...(sym $ wknHomo t (wkn1 m) (keep thin))