1 files changed, 53 insertions, 0 deletions
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
index 136c0d4..15de859 100644
--- a/src/Core/Term/Substitution.idr
+++ b/src/Core/Term/Substitution.idr
@@ -363,3 +363,56 @@ substWkn (App t u) thin sub = cong2 App (substWkn t thin sub) (substWkn u thin s
 public export
 sub1 : Term sx -> Subst (sx :< n) sx
 sub1 t = Base (id sx) :< (t `Over` id sx)
+
+-- Concrete Cases --------------------------------------------------------------
+
+export
+wknSub1 :
+  (t : Term (sx :< n)) ->
+  (u : Term sx) ->
+  (thin : sx `Thins` sy) ->
+  wkn (subst t (sub1 u)) thin = subst (wkn t (keep thin n)) (sub1 (wkn u thin))
+wknSub1 t u thin =
+  let
+    eq0 : (thin . id sx = id sy . thin)
+    eq0  = Calc $
+      |~ thin . id sx
+      ~~ thin          ...(compRightIdentity thin)
+      ~~ id sy . thin  ...(sym $ compLeftIdentity thin)
+
+    eq1 : (Base (thin . id sx) = restrict thin (Base (id sy)))
+    eq1 = Calc $
+      |~ Base (thin . id sx)
+      ~~ Base (id sy . thin)          ...(cong Base eq0)
+      ~~ restrict thin (Base (id sy)) ...(sym $ restrictBase thin (id sy))
+
+    eq2 : wkn u (thin . id sx) = wkn (wkn u thin) (id sy)
+    eq2 = Calc $
+      |~ wkn u (thin . id sx)
+      ~~ wkn u (id sy . thin)     ...(cong (wkn u) $ eq0)
+      ~~ wkn (wkn u thin) (id sy) ...(sym $ wknHomo u thin (id sy))
+  in
+  Calc $
+    |~ wkn (subst t (sub1 u)) thin
+    ~~ subst t (Base (thin . id sx) :< (u `Over` thin . id sx))            ...(wknSubst t (sub1 u) thin)
+    ~~ subst t (Base (thin . id sx) :< (wkn u thin `Over` id sy))          ...(substCong t (Base :< eq2))
+    ~~ subst t (restrict thin (Base $ id sy) :< (wkn u thin `Over` id sy)) ...(cong (subst t . (:< (wkn u thin `Over` id sy))) eq1)
+    ~~ subst t (restrict (keep thin n) (sub1 (wkn u thin)))                ...(sym $ cong (subst t) $ restrictKeep thin n _ (wkn u thin `Over` id sy))
+    ~~ subst (wkn t (keep thin n)) (sub1 (wkn u thin))                     ...(sym $ substWkn t (keep thin n) (sub1 (wkn u thin)))
+
+export
+wknEta :
+  (t : Term sx) ->
+  (thin : sx `Thins` sy) ->
+  (0 n : Name) ->
+  wkn (App (wkn t (wkn1 sx n)) (Var Var.here)) (keep thin n) =
+  App (wkn (wkn t thin) (wkn1 sy n)) (Var Var.here)
+wknEta t thin n =
+  cong2 App
+    (Calc $
+      |~ wkn (wkn t (wkn1 sx n)) (keep thin n)
+      ~~ wkn t (keep thin n . wkn1 sx n)       ...(wknHomo t (drop (id sx) n) (keep thin n))
+      ~~ wkn t (drop thin n)                   ...(cong (wkn t) $ compRightWkn1 thin n)
+      ~~ wkn t (wkn1 sy n . thin)              ...(sym $ cong (wkn t) $ compLeftWkn1 thin n)
+      ~~ wkn (wkn t thin) (wkn1 sy n)          ...(sym $ wknHomo t thin (wkn1 sy n)))
+    (cong Var $ wknKeepHereIsHere thin n)