Fully expand thinnings.

This makes adding CoDebruijn syntax simpler. If carrying the lengths of
contexts around is too inefficient, I can always switch back to
truncated thinnings.

7 files changed, 336 insertions, 239 deletions

diff --git a/src/Thinning.idr b/src/Thinning.idr
index a9b724d..f9e76b5 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -2,125 +2,239 @@ module Thinning
 
 import Data.SnocList.Elem
 
+%prefix_record_projections off
+
 -- Definition ------------------------------------------------------------------
 
 public export
-data Thins : SnocList a -> SnocList a -> Type
-public export
-data NotId : Thins sx sy -> Type
-
-data Thins where
-  Id : sx `Thins` sx
+data Thins : SnocList a -> SnocList a -> Type where
+  Empty : [<] `Thins` [<]
   Drop : sx `Thins` sy -> sx `Thins` sy :< z
   Keep :
     (thin : sx `Thins` sy) ->
-    {auto 0 prf : NotId thin} ->
     sx :< z `Thins` sy :< z
 
-data NotId where
-  DropNotId : NotId (Drop thin)
-  KeepNotId : (0 prf : NotId thin) -> NotId (Keep thin)
-
 %name Thins thin
 
--- Smart Constructors ----------------------------------------------------------
+-- Utility ---------------------------------------------------------------------
 
 public export
-keep : sx `Thins` sy -> sx :< z `Thins` sy :< z
-keep Id = Id
-keep (Drop thin) = Keep (Drop thin)
-keep (Keep thin) = Keep (Keep thin)
+data Len : SnocList a -> Type where
+  Z : Len [<]
+  S : Len sx -> Len (sx :< x)
+
+%name Len k, m, n
+
+%hint
+export
+length : (sx : SnocList a) -> Len sx
+length [<] = Z
+length (sx :< x) = S (length sx)
+
+%hint
+export
+lenSrc : sx `Thins` sy -> Len sx
+lenSrc Empty = Z
+lenSrc (Drop thin) = lenSrc thin
+lenSrc (Keep thin) = S (lenSrc thin)
+
+%hint
+export
+lenTgt : sx `Thins` sy -> Len sy
+lenTgt Empty = Z
+lenTgt (Drop thin) = S (lenTgt thin)
+lenTgt (Keep thin) = S (lenTgt thin)
+
+%hint
+export
+lenPred : Len (sx :< x) -> Len sx
+lenPred (S k) = k
+
+export
+Cast (Len sx) Nat where
+  cast Z = 0
+  cast (S k) = S (cast k)
+
+-- Smart Constructors ----------------------------------------------------------
+
+export
+empty : (len : Len sx) => [<] `Thins` sx
+empty {len = Z} = Empty
+empty {len = S k} = Drop empty
 
 public export
-empty : (sx : SnocList a) -> [<] `Thins` sx
-empty [<] = Id
-empty (sx :< x) = Drop (empty sx)
+id : (len : Len sx) => sx `Thins` sx
+id {len = Z} = Empty
+id {len = S k} = Keep id
+
+export
+point : Len sx => Elem ty sx -> [<ty] `Thins` sx
+point Here = Keep empty
+point (There i) = Drop (point i)
 
 -- Operations ------------------------------------------------------------------
 
 public export
 index : sx `Thins` sy -> Elem z sx -> Elem z sy
-index Id i = i
 index (Drop thin) i = There (index thin i)
 index (Keep thin) Here = Here
 index (Keep thin) (There i) = There (index thin i)
 
 public export
 (.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
-compNotId :
-  {0 thin2 : sy `Thins` sz} ->
-  {0 thin1 : sx `Thins` sy} ->
-  NotId thin2 -> NotId thin1 ->
-  NotId (thin2 . thin1)
-
-Id . thin1 = thin1
-(Drop thin2) . thin1 = Drop (thin2 . thin1)
-(Keep thin2) . Id = Keep thin2
-(Keep thin2) . (Drop thin1) = Drop (thin2 . thin1)
-(Keep {prf = prf2} thin2) . (Keep {prf = prf1} thin1) =
-  Keep {prf = compNotId prf2 prf1} (thin2 . thin1)
-
-compNotId DropNotId p = DropNotId
-compNotId (KeepNotId prf) DropNotId = DropNotId
-compNotId (KeepNotId prf) (KeepNotId prf') = KeepNotId (compNotId prf prf')
+Empty . thin1 = thin1
+Drop thin2 . thin1 = Drop (thin2 . thin1)
+Keep thin2 . Drop thin1 = Drop (thin2 . thin1)
+Keep thin2 . Keep thin1 = Keep (thin2 . thin1)
 
--- Properties ------------------------------------------------------------------
+export
+(++) : sx `Thins` sy -> sz `Thins` sw -> sx ++ sz `Thins` sy ++ sw
+thin2 ++ Empty = thin2
+thin2 ++ (Drop thin1) = Drop (thin2 ++ thin1)
+thin2 ++ (Keep thin1) = Keep (thin2 ++ thin1)
+
+-- Commuting Triangles and Coverings -------------------------------------------
+
+data Triangle : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -> Type where
+  EmptyAny : Triangle Empty thin1 thin1
+  DropAny : Triangle thin2 thin1 thin -> Triangle (Drop thin2) thin1 (Drop thin)
+  KeepDrop : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Drop thin1) (Drop thin)
+  KeepKeep : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Keep thin1) (Keep thin)
+
+data Overlap = Covers | Partitions
+
+namespace Covering
+  public export
+  data Covering : Overlap -> sx `Thins` sz -> sy `Thins` sz -> Type where
+    EmptyEmpty : Covering ov Empty Empty
+    DropKeep : Covering ov thin1 thin2 -> Covering ov (Drop thin1) (Keep thin2)
+    KeepDrop : Covering ov thin1 thin2 -> Covering ov (Keep thin1) (Drop thin2)
+    KeepKeep : Covering Covers thin1 thin2 -> Covering Covers (Keep thin1) (Keep thin2)
+
+record Coproduct {sx, sy, sz : SnocList a} (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where
+  constructor MkCoprod
+  {0 sw : SnocList a}
+  {thin1' : sx `Thins` sw}
+  {thin2' : sy `Thins` sw}
+  {thin : sw `Thins` sz}
+  0 left : Triangle thin thin1' thin1
+  0 right : Triangle thin thin2' thin2
+  0 cover : Covering Covers thin1' thin2'
+
+coprod : (thin1 : sx `Thins` sz) -> (thin2 : sy `Thins` sz) -> Coproduct thin1 thin2
+coprod Empty Empty = MkCoprod EmptyAny EmptyAny EmptyEmpty
+coprod (Drop thin1) (Drop thin2) =
+  { left $= DropAny, right $= DropAny } (coprod thin1 thin2)
+coprod (Drop thin1) (Keep thin2) =
+  { left $= KeepDrop, right $= KeepKeep, cover $= DropKeep } (coprod thin1 thin2)
+coprod (Keep thin1) (Drop thin2) =
+  { left $= KeepKeep, right $= KeepDrop, cover $= KeepDrop } (coprod thin1 thin2)
+coprod (Keep thin1) (Keep thin2) =
+  { left $= KeepKeep, right $= KeepKeep, cover $= KeepKeep } (coprod thin1 thin2)
+
+-- Splitting off Contexts ------------------------------------------------------
+
+data Split : (global, local : SnocList a) -> (thin : sx `Thins` global ++ local) -> Type where
+  MkSplit :
+    (thin2 : sx `Thins` global) ->
+    (thin1 : used `Thins` local) ->
+    Split global local (thin2 ++ thin1)
+
+split : Len local -> (thin : sx `Thins` global ++ local) -> Split global local thin
+split Z thin = MkSplit thin Empty
+split (S k) (Drop thin) with (split k thin)
+  split (S k) (Drop .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Drop thin1)
+split (S k) (Keep thin) with (split k thin)
+  split (S k) (Keep .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Keep thin1)
+
+-- Thinned Things --------------------------------------------------------------
 
--- NotId
+public export
+record Thinned (T : SnocList a -> Type) (sx : SnocList a) where
+  constructor Over
+  {0 support : SnocList a}
+  value : T support
+  thin : support `Thins` sx
 
-NotIdUnique : (p, q : NotId thin) -> p = q
-NotIdUnique DropNotId DropNotId = Refl
-NotIdUnique (KeepNotId prf) (KeepNotId prf) = Refl
+public export
+record OverlapPair (overlap : Overlap) (T, U : SnocList a -> Type) (sx : SnocList a) where
+  constructor MakePair
+  left : Thinned T sx
+  right : Thinned U sx
+  0 cover : Covering overlap left.thin right.thin
 
--- index
+public export
+Pair : (T, U : SnocList a -> Type) -> SnocList a -> Type
+Pair = OverlapPair Covers
 
 export
-indexKeepHere : (thin : sx `Thins` sy) -> index (keep thin) Here = Here
-indexKeepHere Id = Refl
-indexKeepHere (Drop thin) = Refl
-indexKeepHere (Keep thin) = Refl
+MkPair : Thinned t sx -> Thinned u sx -> Thinned (OverlapPair Covers t u) sx
+MkPair (t `Over` thin1) (u `Over` thin2) =
+  let cp = coprod thin1 thin2 in
+  MakePair (t `Over` cp.thin1') (u `Over` cp.thin2') cp.cover `Over` cp.thin
+
+public export
+record Binds (local : SnocList a) (T : SnocList a -> Type) (sx : SnocList a) where
+  constructor MakeBound
+  {0 used : SnocList a}
+  value : T (sx ++ used)
+  thin : used `Thins` local
 
 export
-indexKeepThere :
-  (thin : sx `Thins` sy) ->
-  (i : Elem x sx) ->
-  index (keep thin) (There i) = There (index thin i)
-indexKeepThere Id i = Refl
-indexKeepThere (Drop thin) i = Refl
-indexKeepThere (Keep thin) i = Refl
+MkBound : Len local -> Thinned t (sx ++ local) -> Thinned (Binds local t) sx
+MkBound k (value `Over` thin) with (split k thin)
+  MkBound k (value `Over` .(thin2 ++ thin1)) | MkSplit thin2 thin1 =
+    MakeBound value thin1 `Over` thin2
+
+export
+map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx
+map f (value `Over` thin) = f value `Over` thin
+
+%hint
+export
+thinnedLen : Thinned t sx -> Len sx
+thinnedLen (value `Over` thin) = lenTgt thin
+
+-- Properties ------------------------------------------------------------------
+
+export
+lenUnique : (k, m : Len sx) -> k = m
+lenUnique Z Z = Refl
+lenUnique (S k) (S m) = cong S (lenUnique k m)
+
+export
+identityLeft : (len : Len sy) => (thin : sx `Thins` sy) -> id @{len} . thin = thin
+identityLeft {len = Z} thin = Refl
+identityLeft {len = S k} (Drop thin) = cong Drop (identityLeft thin)
+identityLeft {len = S k} (Keep thin) = cong Keep (identityLeft thin)
+
+export
+identityRight : (len : Len sx) => (thin : sx `Thins` sy) -> thin . id @{len} = thin
+identityRight {len = Z} Empty = Refl
+identityRight (Drop thin) = cong Drop (identityRight thin)
+identityRight {len = S k} (Keep thin) = cong Keep (identityRight thin)
 
--- (.)
+export
+identitySquared : (len : Len sx) -> id @{len} . id @{len} = id @{len}
+identitySquared Z = Refl
+identitySquared (S k) = cong Keep (identitySquared k)
 
 export
 assoc :
-  (thin3 : ctx'' `Thins` ctx''') ->
-  (thin2 : ctx' `Thins` ctx'') ->
-  (thin1 : ctx `Thins` ctx') ->
+  (thin3 : sz `Thins` sw) ->
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
   thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
-assoc Id thin2 thin1 = Refl
+assoc Empty thin2 thin1 = Refl
 assoc (Drop thin3) thin2 thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) Id thin1 = Refl
 assoc (Keep thin3) (Drop thin2) thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Keep thin2) Id = Refl
 assoc (Keep thin3) (Keep thin2) (Drop thin1) = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep {prf = prf3} thin3) (Keep {prf = prf2} thin2) (Keep {prf = prf1} thin1) =
-  let
-    eq : (thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1)
-    eq = assoc thin3 thin2 thin1
-    0 prf :
-      (compNotId prf3 (compNotId prf2 prf1) =
-       (rewrite eq in compNotId (compNotId prf3 prf2) prf1))
-    prf = NotIdUnique _ _
-  in
-  rewrite eq in
-  rewrite prf in
-  Refl
-
-export
-identityRight : (thin : sx `Thins` sy) -> thin . Id = thin
-identityRight Id = Refl
-identityRight (Drop thin) = cong Drop (identityRight thin)
-identityRight (Keep thin) = Refl
+assoc (Keep thin3) (Keep thin2) (Keep thin1) = cong Keep (assoc thin3 thin2 thin1)
+
+export
+indexId : (len : Len sx) => (i : Elem x sx) -> index (id @{len}) i = i
+indexId {len = S k} Here = Refl
+indexId {len = S k} (There i) = cong There (indexId i)
 
 export
 indexHomo :
@@ -128,31 +242,8 @@ indexHomo :
   (thin1 : sx `Thins` sy) ->
   (i : Elem x sx) ->
   index thin2 (index thin1 i) = index (thin2 . thin1) i
-indexHomo Id thin1 i = Refl
-indexHomo (Drop thin2) thin1 i = cong There $ indexHomo thin2 thin1 i
-indexHomo (Keep thin2) Id i = Refl
-indexHomo (Keep thin2) (Drop thin1) i = cong There $ indexHomo thin2 thin1 i
+indexHomo Empty Empty i impossible
+indexHomo (Drop thin2) thin1 i = cong There (indexHomo thin2 thin1 i)
+indexHomo (Keep thin2) (Drop thin1) i = cong There (indexHomo thin2 thin1 i)
 indexHomo (Keep thin2) (Keep thin1) Here = Refl
-indexHomo (Keep thin2) (Keep thin1) (There i) = cong There $ indexHomo thin2 thin1 i
-
-export
-keepHomo :
-  (thin2 : sy `Thins` sz) ->
-  (thin1 : sx `Thins` sy) ->
-  keep thin2 . keep thin1 = keep (thin2 . thin1)
-keepHomo Id thin1 = Refl
-keepHomo (Drop thin2) Id = rewrite identityRight thin2 in Refl
-keepHomo (Drop thin2) (Drop thin1) = Refl
-keepHomo (Drop thin2) (Keep thin1) = Refl
-keepHomo (Keep thin2) Id = Refl
-keepHomo (Keep thin2) (Drop thin) = Refl
-keepHomo (Keep thin2) (Keep thin) = Refl
-
-export
-keepDrop :
-  (thin2 : sy `Thins` sz) ->
-  (thin1 : sx `Thins` sy) ->
-  keep thin2 . Drop thin1 = Drop (thin2 . thin1)
-keepDrop Id thin1 = Refl
-keepDrop (Drop thin2) thin1 = Refl
-keepDrop (Keep thin2) thin1 = Refl
+indexHomo (Keep thin2) (Keep thin1) (There i) = cong There (indexHomo thin2 thin1 i)
diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr
index 705d74b..1a848c0 100644
--- a/src/Total/Encoded/Util.idr
+++ b/src/Total/Encoded/Util.idr
@@ -22,8 +22,8 @@ namespace Bool
   False = Suc Zero
 
   export
-  If : Term ctx B -> Term ctx ty -> Term ctx ty -> Term ctx ty
-  If t u v = Rec t u (Abs $ wkn v (Drop Id))
+  If : Len ctx => Term ctx B -> Term ctx ty -> Term ctx ty -> Term ctx ty
+  If t u v = Rec t u (Abs $ wkn v (Drop id))
 
 namespace Arb
   export
@@ -112,7 +112,7 @@ namespace Pair
   export
   mapProd :
     {ctx, tys, tys' : SnocList Ty} ->
-    {auto 0 prf : length tys = length tys'} ->
+    {auto 0 prf : SnocList.length tys = SnocList.length tys'} ->
     All (Term ctx) (zipWith (~>) tys tys') ->
     Term ctx (Product tys ~> Product tys')
   mapProd {tys = [<], tys' = [<]} [<] = Abs (Var Here)
@@ -120,8 +120,8 @@ namespace Pair
     Abs' (S Z)
       (\p =>
         App' (lift pair)
-          [<App (wkn (mapProd fs {prf = injective prf}) (Drop Id) . lift fst) p
-          , App (wkn f (Drop Id) . lift snd) p
+          [<App (wkn (mapProd fs {prf = injective prf}) (Drop id) . lift fst) p
+          , App (wkn f (Drop id) . lift snd) p
           ])
 
   replicate : Nat -> a -> SnocList a
@@ -292,9 +292,9 @@ namespace Nat
   Cond ((n, v) :: xs) =
     Abs' (S Z)
       (\t =>
-        If (App' (lift LE) [<t, wkn n (Drop Id)])
-          (App (wkn v (Drop Id)) t)
-          (App (wkn (Cond xs) (Drop Id)) (App' (lift Sub) [<t, wkn n (Drop Id)])))
+        If (App' (lift LE) [<t, wkn n (Drop id)])
+          (App (wkn v (Drop id)) t)
+          (App (wkn (Cond xs) (Drop id)) (App' (lift Sub) [<t, wkn n (Drop id)])))
 
 namespace Data
   public export
@@ -394,7 +394,7 @@ namespace Data
                   (lift $ put {tys = map (flip fillShape N) c} $
                     rewrite forgetMap (flip fillShape N) c in
                     elemMap (flip fillShape N) i)
-                  (App' (lift mapSnd) [<Abs (lift $ enumerate n), wkn t (Drop Id)])))
+                  (App' (lift mapSnd) [<Abs (lift $ enumerate n), wkn t (Drop id)])))
           :: calcData (App (lift snd) t) (Suc Zero)
           )
         ])
@@ -409,8 +409,8 @@ namespace Data
   elim cases = Abs' (S Z)
     (\t =>
       let tags = Suc (App (lift $ project $ There $ There Here) t) in
-      let offset = App (lift $ project $ There Here) (wkn t (Drop $ Drop Id)) in
-      let vals = App (lift $ project $ Here) (wkn t (Drop $ Drop Id)) in
+      let offset = App (lift $ project $ There Here) (wkn t (Drop $ Drop id)) in
+      let vals = App (lift $ project $ Here) (wkn t (Drop $ Drop id)) in
       App'
         (Rec tags
           (lift arb)
@@ -420,7 +420,7 @@ namespace Data
                 (rewrite forgetMap (flip fillShape N) c in
                  gmap
                    (\f =>
-                     wkn f (Drop $ Drop $ Drop Id) .
+                     wkn f (Drop $ Drop $ Drop id) .
                      App (lift mapShape) (rec . App (lift Add) (App offset n)))
                    cases) .
                vals)
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr
index 1ed7276..ebde8d5 100644
--- a/src/Total/LogRel.idr
+++ b/src/Total/LogRel.idr
@@ -178,44 +178,49 @@ allValid :
 allValid help (Var i) sub allRels = index help.var allRels i
 allValid help (Abs t) sub allRels =
   let valid = allValid help t in
-  ( let
+  (let
       rec =
         valid
-          (wknAll sub (Drop Id) :< Var Here)
-          (wknAllRel help allRels (Drop Id) :< help.var Here)
+          (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here)
+          (wknAllRel help allRels (Drop $ id @{termsLen sub}) :< help.var Here)
     in
       help.abs rec
   , \thin, u, rel =>
     let
       eq :
-        (subst (wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)) (Base Id :< u) =
+        (subst
+          (wkn (subst t (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here)) (Keep thin))
+          (Base (id @{length _}) :< u) =
          subst t (wknAll sub thin :< u))
-      eq = Calc $
-        |~ subst (wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)) (Base Id :< u)
-        ~~ subst (subst t (wknAll sub (Drop Id) :< Var Here)) (restrict (Base Id :< u) (keep thin))
-          ...(substWkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin) (Base Id :< u))
-        ~~ subst (subst t (wknAll sub (Drop Id) :< Var Here)) (Base thin :< u)
-          ...(cong (subst (subst t (wknAll sub (Drop Id) :< Var Here))) $ restrictKeep (Base Id) u thin)
-        ~~ subst t ((Base thin :< u) . wknAll sub (Drop Id) :< u)
-          ...(substHomo t (wknAll sub (Drop Id) :< Var Here) (Base thin :< u))
-        ~~ subst t (Base (thin . Id) . sub :< u)
-          ...(cong (subst t . (:< u)) $ compWknAll sub (Base thin :< u) (Drop Id))
-        ~~ subst t (Base thin . sub :< u)
-          ...(cong (subst t . (:< u) . (. sub) . Base) $ identityRight thin)
-        ~~ subst t (wknAll sub thin :< u)
-          ...(cong (subst t . (:< u)) $ baseComp thin sub)
+      eq =
+        rewrite lenUnique (termsLen sub) (length ctx') in
+        Calc $
+          |~ subst (wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin)) (Base id :< u)
+          ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (restrict (Base id :< u) (Keep thin))
+            ...(substWkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin) (Base id :< u))
+          ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (Base thin :< u)
+            ...(cong (subst (subst t (wknAll sub (Drop id) :< Var Here)) . (:< u) . Base) $ identityLeft thin)
+          ~~ subst t ((Base thin :< u) . wknAll sub (Drop id) :< u)
+            ...(substHomo t (wknAll sub (Drop id) :< Var Here) (Base thin :< u))
+          ~~ subst t (Base (thin . id) . sub :< u)
+            ...(cong (subst t . (:< u)) $ compWknAll sub (Base thin :< u) (Drop id))
+          ~~ subst t (Base thin . sub :< u)
+            ...(cong (subst t . (:< u) . (. sub) . Base) $ identityRight thin)
+          ~~ subst t (wknAll sub thin :< u)
+            ...(cong (subst t . (:< u)) $ baseComp thin sub)
     in
       preserve
         (backStepHelper help.step)
         (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel))
         (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)}
           eq
-          AppBeta)
+          (AppBeta (length _)))
   )
 allValid help (App t u) sub allRels =
   let (pt, app) = allValid help t sub allRels in
   let rel = allValid help u sub allRels in
-  rewrite sym $ wknId (subst t sub) in app Id (subst u sub) rel
+  rewrite sym $ wknId @{termsLen sub} (subst t sub) in
+    app (id @{termsLen sub}) (subst u sub) rel
 allValid help Zero sub allRels = help.zero
 allValid help (Suc t) sub allRels =
   let pt = allValid help t sub allRels in
@@ -234,4 +239,5 @@ allRel :
   ValidHelper P ->
   (t : Term ctx ty) ->
   P t
-allRel help t = rewrite sym $ substId t in escape (allValid help t (Base Id) Base)
+allRel help t =
+  rewrite sym $ substId @{length ctx} t in escape (allValid help t (Base $ id @{length ctx}) Base)
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
index b5580b5..266d00d 100644
--- a/src/Total/NormalForm.idr
+++ b/src/Total/NormalForm.idr
@@ -93,8 +93,8 @@ recNf' :
 recNf' Zero n relU relV = backStepsRel relU [<RecZero]
 recNf' (Suc t') n relU relV =
   let rec = recNf' t' (invSuc n) relU relV in
-  let step : Rec (Suc t') u v > App (wkn v Id) (Rec t' u v) = rewrite wknId v in RecSuc in
-  backStepsRel (snd relV Id _ rec) [<step]
+  let step : Rec (Suc t') u v > App (wkn v id) (Rec t' u v) = rewrite wknId v in RecSuc in
+  backStepsRel (snd relV id _ rec) [<step]
 recNf' t'@(Var _) n relU relV =
   let nfU = escape relU in
   let nfV = escape {ty = ty ~> ty} relV in
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index cb13706..b11665b 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -8,7 +8,9 @@ data (>) : Term ctx ty -> Term ctx ty -> Type where
   AbsCong : t > u -> Abs t > Abs u
   AppCong1 : t > u -> App t v > App u v
   AppCong2 : u > v -> App t u > App t v
-  AppBeta : App (Abs t) u > subst t (Base Id :< u)
+  AppBeta :
+    (0 len : Len ctx) ->
+    App (Abs t) u > subst t (Base (id @{len}) :< u)
   SucCong : t > u -> Suc t > Suc u
   RecCong1 : t1 > t2 -> Rec t1 u v > Rec t2 u v
   RecCong2 : u1 > u2 -> Rec t u1 v > Rec t u2 v
@@ -68,27 +70,28 @@ RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step
 -- Properties ------------------------------------------------------------------
 
 lemma :
+  (0 len : Len ctx) ->
   (t : Term (ctx :< ty) ty') ->
   (thin : ctx `Thins` ctx') ->
   (u : Term ctx ty) ->
-  subst (wkn t (keep thin)) (Base Id :< wkn u thin) = wkn (subst t (Base Id :< u)) thin
-lemma t thin u = Calc $
-  |~ subst (wkn t (keep thin)) (Base Id :< wkn u thin)
-  ~~ subst t (restrict (Base Id :< wkn u thin) (keep thin))
-    ...(substWkn t (keep thin) (Base Id :< wkn u thin))
-  ~~ subst t (Base thin :< wkn u thin)
-    ...(cong (subst t) $ restrictKeep (Base Id) (wkn u thin) thin)
-  ~~ subst t (Base (thin . Id) :< wkn u thin)
-    ...(sym $ cong (subst t . (:< wkn u thin) . Base) $ identityRight thin)
-  ~~ wkn (subst t (Base Id :< u)) thin
-    ...(sym $ wknSubst t (Base Id :< u) thin)
+  subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) = wkn (subst t (Base (id @{len}) :< u)) thin
+lemma len t thin u = Calc $
+  |~ subst (wkn t (Keep thin)) (Base id :< wkn u thin)
+  ~~ subst t (restrict (Base id :< wkn u thin) (Keep thin))
+    ...(substWkn t (Keep thin) (Base id :< wkn u thin))
+  ~~ subst t (Base (id . thin) :< wkn u thin)
+    ...(Refl)
+  ~~ subst t (Base (thin . id) :< wkn u thin)
+    ...(cong (subst t . (:< wkn u thin) . Base) $ trans (identityLeft thin) (sym $ identityRight thin))
+  ~~ wkn (subst t (Base id :< u)) thin
+    ...(sym $ wknSubst t (Base id :< u) thin)
 
 export
 wknStep : t > u -> wkn t thin > wkn u thin
 wknStep (AbsCong step) = AbsCong (wknStep step)
 wknStep (AppCong1 step) = AppCong1 (wknStep step)
 wknStep (AppCong2 step) = AppCong2 (wknStep step)
-wknStep (AppBeta {t, u}) {thin} = rewrite sym $ lemma t thin u in AppBeta
+wknStep (AppBeta len {t, u}) {thin} = rewrite sym $ lemma len t thin u in AppBeta _
 wknStep (SucCong step) = SucCong (wknStep step)
 wknStep (RecCong1 step) = RecCong1 (wknStep step)
 wknStep (RecCong2 step) = RecCong2 (wknStep step)
diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
index 084ae3e..6c34250 100644
--- a/src/Total/Syntax.idr
+++ b/src/Total/Syntax.idr
@@ -14,29 +14,17 @@ public export
 tys ~>* ty = foldr (~>) ty tys
 
 public export
-data Len : SnocList Ty -> Type where
-  Z : Len [<]
-  S : Len tys -> Len (tys :< ty)
-
-%name Len k, m, n
-
-public export
-Cast (Len ctx) Nat where
-  cast Z = 0
-  cast (S k) = S (cast k)
-
-public export
-0 Fun : Len tys -> (Ty -> Type) -> Type -> Type
+0 Fun : {sx : SnocList a} -> Len sx -> (a -> Type) -> Type -> Type
 Fun Z arg ret = ret
-Fun (S {ty} k) arg ret = Fun k arg (arg ty -> ret)
+Fun (S {x = ty} k) arg ret = Fun k arg (arg ty -> ret)
 
-after : (k : Len tys) -> (a -> b) -> Fun k p a -> Fun k p b
+after : (k : Len sx) -> (a -> b) -> Fun k p a -> Fun k p b
 after Z f x = f x
 after (S k) f x = after k (f .) x
 
 before :
-  (k : Len tys) ->
-  (forall ty. p ty -> q ty) ->
+  (k : Len sx) ->
+  (forall x. p x -> q x) ->
   Fun k q ret ->
   Fun k p ret
 before Z f x = x
@@ -70,19 +58,20 @@ App' t [<] = t
 App' t (us :< u) = App (App' t us) u
 
 export
-(.) : {ty, ty' : Ty} -> Term ctx (ty' ~> ty'') -> Term ctx (ty ~> ty') -> Term ctx (ty ~> ty'')
-t . u = Abs' (S Z) (\x => App (wkn t (Drop Id)) (App (wkn u (Drop Id)) x))
+(.) : Len ctx => {ty, ty' : Ty} -> Term ctx (ty' ~> ty'') -> Term ctx (ty ~> ty') -> Term ctx (ty ~> ty'')
+t . u = Abs' (S Z) (\x => App (wkn t (Drop id)) (App (wkn u (Drop id)) x))
 
 export
 (.*) :
+  Len ctx =>
   {ty : Ty} ->
   {tys : SnocList Ty} ->
   Term ctx (ty ~> ty') ->
   Term ctx (tys ~>* ty) ->
   Term ctx (tys ~>* ty')
 (.*) {tys = [<]} t u = App t u
-(.*) {tys = tys :< ty''} t u = Abs' (S Z) (\f => wkn t (Drop Id) . f) .*  u
+(.*) {tys = tys :< ty''} t u = Abs' (S Z) (\f => wkn t (Drop id) . f) .*  u
 
 export
 lift : {ctx : SnocList Ty} -> Term [<] ty -> Term ctx ty
-lift t = wkn t (empty ctx)
+lift t = wkn t empty
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index d4da92a..d21ec73 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -29,7 +29,7 @@ data Term : SnocList Ty -> Ty -> Type where
 public export
 wkn : Term ctx ty -> ctx `Thins` ctx' -> Term ctx' ty
 wkn (Var i) thin = Var (index thin i)
-wkn (Abs t) thin = Abs (wkn t $ keep thin)
+wkn (Abs t) thin = Abs (wkn t $ Keep thin)
 wkn (App t u) thin = App (wkn t thin) (wkn u thin)
 wkn Zero thin = Zero
 wkn (Suc t) thin = Suc (wkn t thin)
@@ -42,6 +42,12 @@ data Terms : SnocList Ty -> SnocList Ty -> Type where
 
 %name Terms sub
 
+%hint
+export
+termsLen : Terms ctx' ctx -> Len ctx'
+termsLen (Base thin) = lenTgt thin
+termsLen (sub :< t) = termsLen sub
+
 public export
 index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty
 index (Base thin) i = Var (index thin i)
@@ -56,7 +62,7 @@ wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
 public export
 subst : Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
 subst (Var i) sub = index sub i
-subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop Id) :< Var Here)
+subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop id) :< Var Here)
 subst (App t u) sub = App (subst t sub) (subst u sub)
 subst Zero sub = Zero
 subst (Suc t) sub = Suc (subst t sub)
@@ -65,7 +71,6 @@ subst (Rec t u v) sub = Rec (subst t sub) (subst u sub) (subst v sub)
 public export
 restrict : Terms ctx'' ctx' -> ctx `Thins` ctx' -> Terms ctx'' ctx
 restrict (Base thin') thin = Base (thin' . thin)
-restrict (sub :< t) Id = sub :< t
 restrict (sub :< t) (Drop thin) = restrict sub thin
 restrict (sub :< t) (Keep thin) = restrict sub thin :< t
 
@@ -92,7 +97,7 @@ wknHomo :
 wknHomo (Var i) thin1 thin2 =
   cong Var (indexHomo thin2 thin1 i)
 wknHomo (Abs t) thin1 thin2 =
-  cong Abs $ trans (wknHomo t (keep thin1) (keep thin2)) (cong (wkn t) $ keepHomo thin2 thin1)
+  cong Abs (wknHomo t (Keep thin1) (Keep thin2))
 wknHomo (App t u) thin1 thin2 =
   cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
 wknHomo Zero thin1 thin2 =
@@ -103,8 +108,8 @@ wknHomo (Rec t u v) thin1 thin2 =
   cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2)
 
 export
-wknId : (t : Term ctx ty) -> wkn t Id = t
-wknId (Var i) = Refl
+wknId : Len ctx => (t : Term ctx ty) -> wkn t Thinning.id = t
+wknId (Var i) = cong Var (indexId i)
 wknId (Abs t) = cong Abs (wknId t)
 wknId (App t u) = cong2 App (wknId t) (wknId u)
 wknId Zero = Refl
@@ -136,24 +141,13 @@ indexRestrict :
   (i : Elem ty ctx) ->
   index (restrict sub thin) i = index sub (index thin i)
 indexRestrict thin (Base thin') i = sym $ cong Var $ indexHomo thin' thin i
-indexRestrict Id (sub :< t) i = Refl
 indexRestrict (Drop thin) (sub :< t) i = indexRestrict thin sub i
 indexRestrict (Keep thin) (sub :< t) Here = Refl
 indexRestrict (Keep thin) (sub :< t) (There i) = indexRestrict thin sub i
 
-restrictId : (sub : Terms ctx' ctx) -> restrict sub Id = sub
+restrictId : (len : Len ctx) => (sub : Terms ctx' ctx) -> restrict sub (id @{len}) = sub
 restrictId (Base thin) = cong Base (identityRight thin)
-restrictId (sub :< t) = Refl
-
-export
-restrictKeep :
-  (sub : Terms ctx'' ctx) ->
-  (t : Term ctx'' ty) ->
-  (thin : ctx' `Thins` ctx) ->
-  restrict (sub :< t) (keep thin) = restrict sub thin :< t
-restrictKeep sub t Id = sym $ cong (:< t) $ restrictId sub
-restrictKeep sub t (Drop thin) = Refl
-restrictKeep sub t (Keep thin) = Refl
+restrictId {len = S k} (sub :< t) = cong (:< t) (restrictId sub)
 
 restrictHomo :
   (sub : Terms ctx ctx''') ->
@@ -161,9 +155,7 @@ restrictHomo :
   (thin2 : ctx' `Thins` ctx'') ->
   restrict sub (thin1 . thin2) = restrict (restrict sub thin1) thin2
 restrictHomo (Base thin) thin1 thin2 = cong Base (assoc thin thin1 thin2)
-restrictHomo (sub :< t) Id thin2 = Refl
 restrictHomo (sub :< t) (Drop thin1) thin2 = restrictHomo sub thin1 thin2
-restrictHomo (sub :< t) (Keep thin1) Id = Refl
 restrictHomo (sub :< t) (Keep thin1) (Drop thin2) = restrictHomo sub thin1 thin2
 restrictHomo (sub :< t) (Keep thin1) (Keep thin2) = cong (:< t) $ restrictHomo sub thin1 thin2
 
@@ -173,7 +165,6 @@ wknAllRestrict :
   (thin2 : ctx'' `Thins` ctx''') ->
   restrict (wknAll sub thin2) thin1 = wknAll (restrict sub thin1) thin2
 wknAllRestrict thin1 (Base thin) thin2 = sym $ cong Base $ assoc thin2 thin thin1
-wknAllRestrict Id (sub :< t) thin2 = Refl
 wknAllRestrict (Drop thin) (sub :< t) thin2 = wknAllRestrict thin sub thin2
 wknAllRestrict (Keep thin) (sub :< t) thin2 = cong (:< wkn t thin2) (wknAllRestrict thin sub thin2)
 
@@ -188,16 +179,17 @@ wknSubst :
 wknSubst (Var i) sub thin =
   sym (indexWknAll sub thin i)
 wknSubst (Abs t) sub thin =
+  rewrite lenUnique (termsLen $ wknAll sub thin) (lenTgt thin) in
   cong Abs $ Calc $
-    |~ wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)
-    ~~ subst t (wknAll (wknAll sub (Drop Id)) (keep thin) :< Var (index (keep thin) Here))
-      ...(wknSubst t (wknAll sub (Drop Id) :< Var Here) (keep thin))
-    ~~ subst t (wknAll sub (keep thin . Drop Id) :< Var Here)
-      ...(cong2 (\sub, i => subst t (sub :< Var i)) (wknAllHomo sub (Drop Id) (keep thin)) (indexKeepHere thin))
-    ~~ subst t (wknAll sub (Drop Id . thin) :< Var Here)
-      ...(cong (subst t . (:< Var Here) . wknAll sub) $ trans (keepDrop thin Id) (cong Drop $ identityRight thin))
-    ~~ subst t (wknAll (wknAll sub thin) (Drop Id) :< Var Here)
-      ...(sym $ cong (subst t . (:< Var Here)) $ wknAllHomo sub thin (Drop Id))
+    |~ wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin)
+    ~~ subst t (wknAll (wknAll sub (Drop id)) (Keep thin) :< Var (index (Keep thin) Here))
+      ...(wknSubst t (wknAll sub (Drop id) :< Var Here) (Keep thin))
+    ~~ subst t (wknAll sub (Keep thin . Drop id) :< Var Here)
+      ...(cong (subst t . (:< Var Here)) (wknAllHomo sub (Drop id) (Keep thin)))
+    ~~ subst t (wknAll sub (Drop id . thin) :< Var Here)
+      ...(cong (subst t . (:< Var Here) . wknAll sub . Drop) $ trans (identityRight thin) (sym $ identityLeft thin))
+    ~~ subst t (wknAll (wknAll sub thin) (Drop id) :< Var Here)
+      ...(sym $ cong (subst t . (:< Var Here)) $ wknAllHomo sub thin (Drop id))
 wknSubst (App t u) sub thin =
   cong2 App (wknSubst t sub thin) (wknSubst u sub thin)
 wknSubst Zero sub thin =
@@ -216,14 +208,13 @@ substWkn :
 substWkn (Var i) thin sub =
   sym (indexRestrict thin sub i)
 substWkn (Abs t) thin sub =
+  rewrite lenUnique (termsLen $ restrict sub thin) (termsLen sub) in
   cong Abs $ Calc $
-    |~ subst (wkn t $ keep thin) (wknAll sub (Drop Id) :< Var Here)
-    ~~ subst t (restrict (wknAll sub (Drop Id) :< Var Here) (keep thin))
-      ...(substWkn t (keep thin) (wknAll sub (Drop Id) :< Var Here))
-    ~~ subst t (restrict (wknAll sub (Drop Id)) thin :< Var Here)
-      ...(cong (subst t) $ restrictKeep (wknAll sub (Drop Id)) (Var Here) thin)
-    ~~ subst t (wknAll (restrict sub thin) (Drop Id) :< Var Here)
-      ...(cong (subst t . (:< Var Here)) $ wknAllRestrict thin sub (Drop Id))
+    |~ subst (wkn t $ Keep thin) (wknAll sub (Drop id) :< Var Here)
+    ~~ subst t (restrict (wknAll sub (Drop id)) thin :< Var Here)
+      ...(substWkn t (Keep thin) (wknAll sub (Drop id) :< Var Here))
+    ~~ subst t (wknAll (restrict sub thin) (Drop id) :< Var Here)
+      ...(cong (subst t . (:< Var Here)) $ wknAllRestrict thin sub (Drop id))
 substWkn (App t u) thin sub =
   cong2 App (substWkn t thin sub) (substWkn u thin sub)
 substWkn Zero thin sub =
@@ -236,26 +227,37 @@ substWkn (Rec t u v) thin sub =
 namespace Equiv
   public export
   data Equiv : Terms ctx' ctx -> Terms ctx' ctx -> Type where
-    Base : Equiv (Base (keep thin)) (Base (Drop thin) :< Var Here)
+    Base : Equiv (Base (Keep thin)) (Base (Drop thin) :< Var Here)
     WknAll :
+      (len : Len ctx) =>
       Equiv sub sub' ->
-      Equiv (wknAll sub (Drop Id) :< Var Here) (wknAll sub' (Drop Id) :< Var Here)
+      Equiv
+        (wknAll sub (Drop $ id @{len}) :< Var Here)
+        (wknAll sub' (Drop $ id @{len}) :< Var Here)
 
   %name Equiv prf
 
 indexCong : Equiv sub sub' -> (i : Elem ty ctx) -> index sub i = index sub' i
-indexCong Base Here = irrelevantEq $ cong Var (indexKeepHere _)
-indexCong Base (There i) = irrelevantEq $ cong Var (indexKeepThere _ i)
+indexCong Base Here = Refl
+indexCong Base (There i) = Refl
 indexCong (WknAll prf) Here = Refl
 indexCong (WknAll {sub, sub'} prf) (There i) = Calc $
-  |~ index (wknAll sub (Drop Id)) i
-  ~~ wkn (index sub i) (Drop Id)     ...(indexWknAll sub (Drop Id) i)
-  ~~ wkn (index sub' i) (Drop Id)    ...(cong (flip wkn (Drop Id)) $ indexCong prf i)
-  ~~ index (wknAll sub' (Drop Id)) i ...(sym $ indexWknAll sub' (Drop Id) i)
+  |~ index (wknAll sub (Drop id)) i
+  ~~ wkn (index sub i) (Drop id)     ...(indexWknAll sub (Drop id) i)
+  ~~ wkn (index sub' i) (Drop id)    ...(cong (flip wkn (Drop id)) $ indexCong prf i)
+  ~~ index (wknAll sub' (Drop id)) i ...(sym $ indexWknAll sub' (Drop id) i)
 
-substCong : (t : Term ctx ty) -> Equiv sub sub' -> subst t sub = subst t sub'
+substCong :
+  (len : Len ctx') =>
+  (t : Term ctx ty) ->
+  {0 sub, sub' : Terms ctx' ctx} ->
+  Equiv sub sub' ->
+  subst t sub = subst t sub'
 substCong (Var i) prf = indexCong prf i
-substCong (Abs t) prf = cong Abs (substCong t (WknAll prf))
+substCong (Abs t) prf =
+  rewrite lenUnique (termsLen sub) (termsLen sub') in
+  rewrite lenUnique (termsLen sub') len in
+  cong Abs (substCong t (WknAll prf))
 substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf)
 substCong Zero prf = Refl
 substCong (Suc t) prf = cong Suc (substCong t prf)
@@ -263,10 +265,12 @@ substCong (Rec t u v) prf = cong3 Rec (substCong t prf) (substCong u prf) (subst
 
 substBase : (t : Term ctx ty) -> (thin : ctx `Thins` ctx') -> subst t (Base thin) = wkn t thin
 substBase (Var i) thin = Refl
-substBase (Abs t) thin = cong Abs $ Calc $
-  |~ subst t (Base (Drop thin) :< Var Here)
-  ~~ subst t (Base $ keep thin)             ...(sym $ substCong t Base)
-  ~~ wkn t (keep thin)                      ...(substBase t (keep thin))
+substBase (Abs t) thin =
+  rewrite identityLeft thin in
+  cong Abs $ Calc $
+    |~ subst t (Base (Drop thin) :< Var Here)
+    ~~ subst t (Base $ Keep thin)             ...(sym $ substCong t Base)
+    ~~ wkn t (Keep thin)                      ...(substBase t (Keep thin))
 substBase (App t u) thin = cong2 App (substBase t thin) (substBase u thin)
 substBase Zero thin = Refl
 substBase (Suc t) thin = cong Suc (substBase t thin)
@@ -322,9 +326,12 @@ baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
 -- Substitution
 
 export
-substId : (t : Term ctx ty) -> subst t (Base Id) = t
-substId (Var i) = Refl
-substId (Abs t) = cong Abs $ trans (sym $ substCong t Base) (substId t)
+substId : (len : Len ctx) => (t : Term ctx ty) -> subst t (Base $ id @{len}) = t
+substId (Var i) = cong Var (indexId i)
+substId (Abs t) =
+  rewrite lenUnique (termsLen $ Base $ id @{len}) len in
+  rewrite identitySquared len in
+  cong Abs $ trans (sym $ substCong t Base) (substId t)
 substId (App t u) = cong2 App (substId t) (substId u)
 substId Zero = Refl
 substId (Suc t) = cong Suc (substId t)
@@ -339,18 +346,19 @@ substHomo :
 substHomo (Var i) sub1 sub2 =
   sym $ indexComp sub1 sub2 i
 substHomo (Abs t) sub1 sub2 =
+  rewrite lenUnique (termsLen $ sub2 . sub1) (termsLen sub2) in
   cong Abs $ Calc $
-    |~ subst (subst t (wknAll sub1 (Drop Id) :< Var Here)) (wknAll sub2 (Drop Id) :< Var Here)
-    ~~ subst t ((wknAll sub2 (Drop Id) :< Var Here) . (wknAll sub1 (Drop Id) :< Var Here))
-      ...(substHomo t (wknAll sub1 (Drop Id) :< Var Here) (wknAll sub2 (Drop Id) :< Var Here))
-    ~~ subst t ((wknAll sub2 (Drop Id) :< Var Here) . wknAll sub1 (Drop Id) :< Var Here)
+    |~ subst (subst t (wknAll sub1 (Drop id) :< Var Here)) (wknAll sub2 (Drop id) :< Var Here)
+    ~~ subst t ((wknAll sub2 (Drop id) :< Var Here) . (wknAll sub1 (Drop id) :< Var Here))
+      ...(substHomo t (wknAll sub1 (Drop id) :< Var Here) (wknAll sub2 (Drop id) :< Var Here))
+    ~~ subst t ((wknAll sub2 (Drop id) :< Var Here) . wknAll sub1 (Drop id) :< Var Here)
       ...(Refl)
-    ~~ subst t (restrict (wknAll sub2 (Drop Id)) Id . sub1 :< Var Here)
-      ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop Id) (wknAll sub2 (Drop Id) :< Var Here))
-    ~~ subst t (wknAll sub2 (Drop Id) . sub1 :< Var Here)
-      ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop Id)))
-    ~~ subst t (wknAll (sub2 . sub1) (Drop Id) :< Var Here)
-      ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop Id))
+    ~~ subst t (restrict (wknAll sub2 (Drop id)) id . sub1 :< Var Here)
+      ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop id) (wknAll sub2 (Drop id) :< Var Here))
+    ~~ subst t (wknAll sub2 (Drop id) . sub1 :< Var Here)
+      ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop id)))
+    ~~ subst t (wknAll (sub2 . sub1) (Drop id) :< Var Here)
+      ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop id))
 substHomo (App t u) sub1 sub2 =
   cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2)
 substHomo Zero sub1 sub2 =