WIP : use smarter weakenings.better-thinning

11 files changed, 1464 insertions, 930 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index 2456685..5ef6ae7 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -7,7 +7,9 @@ options = "--total"
 depends = contrib
 
 modules
-  = Thinning
+  = Subst
+  , Thinning
+  , Total.Encoded.Test
   , Total.Encoded.Util
   , Total.LogRel
   , Total.NormalForm
diff --git a/src/Subst.idr b/src/Subst.idr
new file mode 100644
index 0000000..08220e7
--- /dev/null
+++ b/src/Subst.idr
@@ -0,0 +1,460 @@
+module Subst
+
+import Control.Order
+import Control.Relation
+import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Generic
+import Thinning
+
+%prefix_record_projections off
+
+-- Interfaces ------------------------------------------------------------------
+
+public export
+interface Point (0 a : Type) (0 t : a -> SnocList a -> Type) | t where
+  point : {0 x : a} -> {0 sx : SnocList a} -> Elem x sx -> t x sx
+
+public export
+interface Weaken (0 a : Type) (0 t : a -> SnocList a -> Type) | t where
+  wkn :
+    {0 x : a} ->
+    {0 sx, sy : SnocList a} ->
+    t x sx ->
+    sx `Thins` sy ->
+    t x sy
+  shift : {0 x, y : a} -> {0 sx : SnocList a} -> t y sx -> t y (sx :< x)
+  shift v = wkn v (drop (id sx) x)
+
+public export
+interface Point a t => Weaken a t => PointWeaken a t | t where
+
+public export
+interface Weaken a t => FullWeaken a t | t where
+  wknId : {0 x : a} -> {0 sx : SnocList a} -> (v : t x sx) -> wkn v (id sx) = v
+  wknHomo :
+    {0 x : a} ->
+    {0 sx, sy, sz : SnocList a} ->
+    (v : t x sx) ->
+    (thin1 : sx `Thins` sy) ->
+    (thin2 : sy `Thins` sz) ->
+    wkn (wkn v thin1) thin2 = wkn v (thin2 . thin1)
+  shiftIsWkn :
+    {0 x, y : a} ->
+    {0 sx : SnocList a} ->
+    (v : t y sx) ->
+    wkn v (drop (id sx) x) = shift v
+
+public export
+interface Point a t => FullWeaken a t => FullPointWeaken a t | t where
+  wknPoint :
+    {0 x : a} ->
+    {0 sx, sy : SnocList a} ->
+    (i : Elem x sx) ->
+    (thin : sx `Thins` sy) ->
+    wkn {t} (point i) thin = point (index thin i)
+
+-- Substitutions ---------------------------------------------------------------
+
+public export
+data Subst : (t : a -> SnocList a -> Type) -> (sx, sy : SnocList a) -> Type where
+  Base : sx `Thins` sy -> Subst t sx sy
+  (:<) : Subst t sx sy -> t x sy -> Subst t (sx :< x) sy
+
+%name Subst sub
+
+export
+index : Point a t => Subst t sx sy -> Elem x sx -> t x sy
+index (Base thin) i = point (index thin i)
+index (sub :< v) Here = v
+index (sub :< v) (There i) = index sub i
+
+namespace Subst
+  export
+  wkn : Weaken a t => Subst t sx sy -> sy `Thins` sz -> Subst t sx sz
+  wkn (Base thin') thin = Base (thin . thin')
+  wkn (sub :< v) thin = wkn sub thin :< wkn v thin
+
+  export
+  shift : Weaken a t => Subst t sx sy -> Subst t sx (sy :< y)
+  shift (Base thin) = Base (drop thin y)
+  shift (sub :< v) = shift sub :< shift v
+
+  public export
+  lift : Point a t => Weaken a t => Subst t sx sy -> Subst t (sx :< z) (sy :< z)
+  lift sub = shift sub :< point Here
+
+export
+restrict : Subst t sy sz -> sx `Thins` sy -> Subst t sx sz
+restrictView :
+  Subst t sy sz ->
+  t y sz ->
+  {0 thin : sx `Thins` sy :< y} ->
+  View thin ->
+  Subst t sx sz
+
+restrict (Base thin') thin = Base (thin' . thin)
+restrict (sub :< v) thin = restrictView sub v (view thin)
+
+restrictView sub v Id = sub :< v
+restrictView sub v (Drop thin z) = restrict sub thin
+restrictView sub v (Keep thin z) = restrict sub thin :< v
+
+-- Equivalence -----------------------------------------------------------------
+
+public export
+record Equiv {auto 0 p : Point a t} (sub1, sub2 : Subst t sx sy) where
+  constructor IsEquiv
+  equiv : (forall x. (i : Elem x sx) -> index sub1 i = index sub2 i)
+
+%name Subst.Equiv e
+
+export
+Point a t => Reflexive (Subst t sx sy) Equiv where
+  reflexive = IsEquiv (\i => Refl)
+
+export
+Point a t => Symmetric (Subst t sx sy) Equiv where
+  symmetric e = IsEquiv (\i => sym (e.equiv i))
+
+export
+Point a t => Transitive (Subst t sx sy) Equiv where
+  transitive e e' = IsEquiv (\i => trans (e.equiv i) (e'.equiv i))
+
+export
+Point a t => Preorder (Subst t sx sy) Equiv where
+
+namespace Equiv
+  export
+  Base :
+    (p : Point a t) =>
+    {0 thin1, thin2 : sx `Thins` sy} ->
+    thin1 = thin2 ->
+    Equiv @{p} (Base thin1) (Base thin2)
+  Base prf = IsEquiv (\i => cong (\thin => index (Base thin) i) prf)
+
+  export
+  (:<) :
+    Point a t =>
+    {0 sub1, sub2 : Subst t sx sy} ->
+    Equiv sub1 sub2 ->
+    u = v ->
+    Equiv (sub1 :< u) (sub2 :< v)
+  e :< prf = IsEquiv (\i => case i of Here => prf; There i => e.equiv i)
+
+-- Properties ------------------------------------------------------------------
+
+export
+irrelevantEquiv :
+  Point a t =>
+  {0 sub1, sub2 : Subst t sx sy} ->
+  (0 _ : Equiv sub1 sub2) ->
+  Equiv sub1 sub2
+irrelevantEquiv e = IsEquiv (\i => irrelevantEq $ e.equiv i)
+
+-- Weakening
+
+namespace Subst
+  export
+  indexWkn :
+    FullPointWeaken a t =>
+    (sub : Subst t sx sy) ->
+    (thin : sy `Thins` sz) ->
+    (i : Elem x sx) ->
+    wkn (index sub i) thin = index (wkn sub thin) i
+  indexWkn (Base thin') thin i = Calc $
+    |~ wkn (point (index thin' i)) thin
+    ~~ point {t} (index thin (index thin' i)) ...(wknPoint (index thin' i) thin)
+    ~~ point (index (thin . thin') i)         ...(cong point $ indexHomo thin' thin i)
+  indexWkn (sub :< v) thin Here = Refl
+  indexWkn (sub :< v) thin (There i) = indexWkn sub thin i
+
+  export
+  wknCong :
+    FullPointWeaken a t =>
+    {0 sub1, sub2 : Subst t sx sy} ->
+    {0 thin1, thin2 : sy `Thins` sz} ->
+    Equiv sub1 sub2 ->
+    thin1 = thin2 ->
+    Equiv (wkn sub1 thin1) (wkn sub2 thin2)
+  wknCong e prf = irrelevantEquiv $ IsEquiv (\i => Calc $
+    |~ index (wkn sub1 thin1) i
+    ~~ wkn (index sub1 i) thin1 ..<(indexWkn sub1 thin1 i)
+    ~~ wkn (index sub2 i) thin2 ...(cong2 wkn (e.equiv i) prf)
+    ~~ index (wkn sub2 thin2) i ...(indexWkn sub2 thin2 i))
+
+  export
+  wknId :
+    FullPointWeaken a t =>
+    (sub : Subst t sx sy) ->
+    Equiv (wkn sub (id sy)) sub
+  wknId (Base thin) = Base (identityLeft thin)
+  wknId (sub :< v) = wknId sub :< wknId v
+
+  export
+  wknHomo :
+    FullPointWeaken a t =>
+    (sub : Subst t sx sy) ->
+    (thin1 : sy `Thins` sz) ->
+    (thin2 : sz `Thins` sw) ->
+    Equiv (wkn (wkn sub thin1) thin2) (wkn sub (thin2 . thin1))
+  wknHomo (Base thin) thin1 thin2 = Base (assoc thin2 thin1 thin)
+  wknHomo (sub :< v) thin1 thin2 = wknHomo sub thin1 thin2 :< wknHomo v thin1 thin2
+
+-- Restrict
+
+export
+restrictBase :
+  (p : Point a t) =>
+  (thin' : sy `Thins` sz) ->
+  (thin : sx `Thins` sy) ->
+  Equiv @{p} (Base (thin' . thin)) (restrict (Base thin') thin)
+restrictBase thin' thin = reflexive
+
+export
+indexRestrict :
+  Point a t =>
+  (sub : Subst t sy sz) ->
+  (thin : sx `Thins` sy) ->
+  (i : Elem x sx) ->
+  index sub (index thin i) = index (restrict sub thin) i
+indexRestrictView :
+  Point a t =>
+  (sub : Subst t sy sz) ->
+  (v : t y sz) ->
+  {0 thin : sx `Thins` sy :< y} ->
+  (view : View thin) ->
+  (i : Elem x sx) ->
+  index (sub :< v) (index thin i) = index (restrictView sub v view) i
+
+indexRestrict (Base thin') thin i = cong point (indexHomo thin thin' i)
+indexRestrict (sub :< v) thin i = indexRestrictView sub v (view thin) i
+
+indexRestrictView sub v Id i = cong (index (sub :< v)) (indexId i)
+indexRestrictView sub v (Drop thin z) i = Calc $
+  |~ index (sub :< v) (index (drop thin z) i)
+  ~~ index (sub :< v) (There (index thin i))  ...(cong (index (sub :< v)) $ indexDrop thin i)
+  ~~ index sub (index thin i)                 ...(Refl)
+  ~~ index (restrict sub thin) i              ...(indexRestrict sub thin i)
+indexRestrictView sub v (Keep thin x) Here = cong (index (sub :< v)) (indexKeepHere thin)
+indexRestrictView sub v (Keep thin z) (There i) = Calc $
+  |~ index (sub :< v) (index (keep thin z) (There i))
+  ~~ index (sub :< v) (There (index thin i))          ...(cong (index (sub :< v)) $ indexKeepThere thin i)
+  ~~ index sub (index thin i)                         ...(Refl)
+  ~~ index (restrict sub thin) i                      ...(indexRestrict sub thin i)
+
+export
+restrictCong :
+  Point a t =>
+  {0 sub1, sub2 : Subst t sy sz} ->
+  {0 thin1, thin2 : sx `Thins` sy} ->
+  Equiv sub1 sub2 ->
+  thin1 = thin2 ->
+  Equiv (restrict sub1 thin1) (restrict sub2 thin2)
+restrictCong e prf = irrelevantEquiv $ IsEquiv (\i => Calc $
+  |~ index (restrict sub1 thin1) i
+  ~~ index sub1 (index thin1 i)    ..<(indexRestrict sub1 thin1 i)
+  ~~ index sub2 (index thin1 i)    ...(e.equiv (index thin1 i))
+  ~~ index sub2 (index thin2 i)    ...(cong (\thin => index sub2 (index thin i)) prf)
+  ~~ index (restrict sub2 thin2) i ...(indexRestrict sub2 thin2 i))
+
+export
+restrictId :
+  Point a t =>
+  (sub : Subst t sx sy) ->
+  Equiv (restrict sub (id sx)) sub
+restrictId (Base thin) = Base (identityRight thin)
+restrictId {sx = .(sx :< x)} (sub :< v) =
+  rewrite viewUnique (view (id (sx :< x))) Id in
+  reflexive
+
+export
+restrictHomo :
+  Point a t =>
+  (sub : Subst t sz sw) ->
+  (thin1 : sy `Thins` sz) ->
+  (thin2 : sx `Thins` sy) ->
+  Equiv (restrict (restrict sub thin1) thin2) (restrict sub (thin1 . thin2))
+restrictViewHomo1 :
+  Point a t =>
+  (sub : Subst t sz sw) ->
+  (v : t z sw) ->
+  {0 thin1 : sy `Thins` sz :< z} ->
+  (view1 : View thin1) ->
+  (thin2 : sx `Thins` sy) ->
+  Equiv (restrict (restrictView sub v view1) thin2) (restrictView sub v (view (thin1 . thin2)))
+restrictViewHomo2 :
+  Point a t =>
+  (sub : Subst t sz sw) ->
+  (v : t y sw) ->
+  (thin1 : sy `Thins` sz) ->
+  {auto 0 ok : NotId thin1} ->
+  {0 thin2 : sx `Thins` sy :< y} ->
+  (view2 : View thin2) ->
+  Equiv
+    (restrictView (restrict sub thin1) v view2)
+    (restrictView sub v (view (keep thin1 y . thin2)))
+
+restrictHomo (Base thin) thin1 thin2 = symmetric $ Base (assoc thin thin1 thin2)
+restrictHomo (sub :< v) thin1 thin2 = restrictViewHomo1 sub v (view thin1) thin2
+
+restrictViewHomo1 sub v Id thin2 =
+  rewrite identityLeft thin2 in
+  reflexive
+restrictViewHomo1 sub v (Drop thin1 z) thin2 =
+  rewrite dropLeft thin1 thin2 z in
+  rewrite viewUnique (view (drop (thin1 . thin2) z)) (Drop (thin1 . thin2) z) in
+  restrictHomo sub thin1 thin2
+restrictViewHomo1 sub v (Keep thin1 z) thin2 = restrictViewHomo2 sub v thin1 (view thin2)
+
+restrictViewHomo2 sub v thin1 Id =
+  rewrite identityRight (keep thin1 y) in
+  rewrite viewUnique (view (keep thin1 y)) (Keep thin1 y) in
+  reflexive
+restrictViewHomo2 sub v thin1 (Drop thin2 y) =
+  rewrite keepDrop thin1 thin2 y in
+  rewrite viewUnique (view (drop (thin1 . thin2) y)) (Drop (thin1 . thin2) y) in
+  restrictHomo sub thin1 thin2
+restrictViewHomo2 sub v thin1 (Keep thin2 {ok = ok'} y) =
+  rewrite keepHomo thin1 thin2 y in
+  rewrite
+    viewUnique
+      (view (keep (thin1 . thin2) y))
+      (Keep (thin1 . thin2) {ok = compNotId ok ok'} y)
+  in
+  restrictHomo sub thin1 thin2 :< Refl
+
+namespace Subst
+  export
+  wknRestrict :
+    FullPointWeaken a t =>
+    (sub : Subst t sy sz) ->
+    (thin1 : sx `Thins` sy) ->
+    (thin2 : sz `Thins` sw) ->
+    Equiv (wkn (restrict sub thin1) thin2) (restrict (wkn sub thin2) thin1)
+  wknRestrictView :
+    FullPointWeaken a t =>
+    (sub : Subst t sy sz) ->
+    (v : t y sz) ->
+    {0 thin1 : sx `Thins` sy :< y} ->
+    (view1 : View thin1) ->
+    (thin2 : sz `Thins` sw) ->
+    Equiv (wkn (restrictView sub v view1) thin2) (restrictView (wkn sub thin2) (wkn v thin2) view1)
+
+  wknRestrict (Base thin) thin1 thin2 = Base (assoc thin2 thin thin1)
+  wknRestrict (sub :< v) thin1 thin2 = wknRestrictView sub v (view thin1) thin2
+
+  wknRestrictView sub v Id thin2 = reflexive
+  wknRestrictView sub v (Drop thin1 y) thin2 = wknRestrict sub thin1 thin2
+  wknRestrictView sub v (Keep thin1 y) thin2 = wknRestrict sub thin1 thin2 :< Refl
+
+-- Shift
+
+  export
+  shiftIsWkn :
+    Point a t =>
+    FullWeaken a t =>
+    (sub : Subst t sx sy) ->
+    Equiv (wkn sub (drop (id sy) y)) (shift sub)
+  shiftIsWkn (Base thin) =
+    Base $ trans
+      (dropLeft (id sy) thin y)
+      (cong (\thin => drop thin y) $ identityLeft thin)
+  shiftIsWkn (sub :< v) = shiftIsWkn sub :< shiftIsWkn v
+
+export
+shiftCong :
+  FullPointWeaken a t =>
+  {0 sub1, sub2 : Subst t sx sy} ->
+  Equiv sub1 sub2 ->
+  Equiv (shift {y} sub1) (shift sub2)
+shiftCong e = irrelevantEquiv $ CalcWith $
+  |~ shift sub1
+  <~ wkn sub1 (drop (id sy) y) ..<(shiftIsWkn sub1)
+  <~ wkn sub2 (drop (id sy) y) ...(wknCong e reflexive)
+  <~ shift sub2                ...(shiftIsWkn sub2)
+
+export
+wknShiftKeep :
+  FullPointWeaken a t =>
+  (sub : Subst t sx sy) ->
+  (thin : sy `Thins` sz) ->
+  Equiv (wkn (shift sub) (keep thin y)) (shift (wkn sub thin))
+wknShiftKeep sub thin = CalcWith $
+  |~ wkn (shift sub) (keep thin y)
+  <~ wkn (wkn sub (drop (id sy) y)) (keep thin y) ..<(wknCong (shiftIsWkn sub) reflexive)
+  <~ wkn sub (keep thin y . drop (id sy) y)       ...(wknHomo sub (drop (id sy) y) (keep thin y))
+  ~~ wkn sub (drop (thin . (id sy)) y)            ...(cong (wkn sub) (keepDrop thin (id sy) y))
+  ~~ wkn sub (drop thin y)                        ...(cong (\thin => wkn sub (drop thin y)) (identityRight thin))
+  ~~ wkn sub (drop (id sz . thin) y)              ..<(cong (\thin => wkn sub (drop thin y)) (identityLeft thin))
+  <~ wkn sub (drop (id sz) y . thin)              ..<(wknCong reflexive (dropLeft (id sz) thin y))
+  <~ wkn (wkn sub thin) (drop (id sz) y)          ..<(wknHomo sub thin (drop (id sz) y))
+  <~ shift (wkn sub thin)                         ...(shiftIsWkn (wkn sub thin))
+
+
+export
+restrictShift :
+  FullPointWeaken a t =>
+  (sub : Subst t sy sz) ->
+  (thin : sx `Thins` sy) ->
+  Equiv (restrict (shift {y = z} sub) thin) (shift (restrict sub thin))
+restrictShift sub thin = CalcWith $
+  |~ restrict (shift sub) thin
+  <~ restrict (wkn sub (drop (id sz) z)) thin ..<(restrictCong (shiftIsWkn sub) reflexive)
+  <~ wkn (restrict sub thin) (drop (id sz) z) ..<(wknRestrict sub thin (drop (id sz) z))
+  <~ shift (restrict sub thin)                ...(shiftIsWkn (restrict sub thin))
+
+-- Lift
+
+namespace Subst
+  export
+  liftCong :
+    FullPointWeaken a t =>
+    {0 sub1, sub2 : Subst t sx sy} ->
+    Equiv sub1 sub2 ->
+    Equiv (lift sub1) (lift sub2)
+  liftCong e = shiftCong e :< Refl
+
+  export
+  wknLift :
+    FullPointWeaken a t =>
+    (sub : Subst t sx sy) ->
+    (thin : sy `Thins` sz) ->
+    Equiv (wkn (lift sub) (keep thin z)) (lift (wkn sub thin))
+  wknLift sub thin =
+    wknShiftKeep sub thin :<
+    trans
+      (wknPoint Here (keep thin z))
+      (cong point $ indexKeepHere thin)
+
+  restrictLiftView :
+    FullPointWeaken a t =>
+    (sub : Subst t sy sz) ->
+    {0 thin : sx `Thins` sy} ->
+    (view : View thin) ->
+    Equiv (restrict (lift sub) (keep thin y)) (lift (restrict sub thin))
+  restrictLiftView sub Id =
+    rewrite keepId sy y in
+    rewrite viewUnique (view (id (sy :< y))) Id in
+    symmetric (shiftCong (restrictId sub)) :< Refl
+  restrictLiftView sub (Drop thin z) =
+    rewrite
+      viewUnique
+        (view (keep (drop thin z) y))
+        (Keep (drop thin z) {ok = dropNotId thin z} y)
+    in
+    restrictShift sub (drop thin z) :< Refl
+  restrictLiftView sub (Keep thin z) =
+    rewrite
+      viewUnique
+        (view (keep (keep thin z) y))
+        (Keep (keep thin z) {ok = keepNotId thin z} y)
+    in
+    restrictShift sub (keep thin z) :< Refl
+
+  export
+  restrictLift :
+    FullPointWeaken a t =>
+    (sub : Subst t sy sz) ->
+    (thin : sx `Thins` sy) ->
+    Equiv (restrict (lift sub) (keep thin y)) (lift (restrict sub thin))
+  restrictLift sub thin = restrictLiftView sub (view thin)
diff --git a/src/Thinning.idr b/src/Thinning.idr
index d2d65df..b7a479e 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -1,149 +1,298 @@
 module Thinning
 
-import Data.Singleton
-import Data.SnocList.Elem
+import public Data.SnocList.Elem
+
+import Syntax.PreorderReasoning
 
 %prefix_record_projections off
 
 -- Definition ------------------------------------------------------------------
 
-public export
-data Thins : SnocList a -> SnocList a -> Type where
-  Empty : [<] `Thins` [<]
-  Drop : sx `Thins` sy -> sx `Thins` sy :< z
+export
+data Thins : SnocList a -> SnocList a -> Type
+export
+data NotId : sx `Thins` sy -> Type
+
+data Thins where
+  Id : sx `Thins` sx
+  Drop : sx `Thins` sy -> sx `Thins` sy :< y
   Keep :
     (thin : sx `Thins` sy) ->
+    {auto 0 ok : NotId thin} ->
     sx :< z `Thins` sy :< z
 
-%name Thins thin
+data NotId where
+  DropNotId : NotId (Drop thin)
+  KeepNotId : NotId thin -> NotId (Keep thin)
 
--- Utility ---------------------------------------------------------------------
+%name Thins thin
 
-public export
-data Len : SnocList a -> Type where
-  Z : Len [<]
-  S : Len sx -> Len (sx :< x)
+-- Smart Constructors ----------------------------------------------------------
 
-%name Len k, m, n
+export
+id : (0 sx : SnocList a) -> sx `Thins` sx
+id sx = Id
 
-%hint
-public export
-length : (sx : SnocList a) -> Len sx
-length [<] = Z
-length (sx :< x) = S (length sx)
+export
+drop : sx `Thins` sy -> (0 z : a) -> sx `Thins` sy :< z
+drop thin z = Drop thin
 
-%hint
 export
-lenAppend : Len sx -> Len sy -> Len (sx ++ sy)
-lenAppend k Z = k
-lenAppend k (S m) = S (lenAppend k m)
+keep : sx `Thins` sy -> (0 z : a) -> sx :< z `Thins` sy :< z
+keep Id z = Id
+keep (Drop thin) z = Keep (Drop thin)
+keep (Keep thin) z = Keep (Keep thin)
+
+-- Views -----------------------------------------------------------------------
+
+notIdUnique : (p, q : NotId thin) -> p = q
+notIdUnique DropNotId DropNotId = Refl
+notIdUnique (KeepNotId p) (KeepNotId p) = Refl
+
+keepIsKeep :
+  (thin : sx `Thins` sy) ->
+  {auto 0 ok : NotId thin} ->
+  (0 z : a) ->
+  keep thin z = Keep {ok} thin
+keepIsKeep (Drop thin) z =
+  rewrite notIdUnique ok DropNotId in Refl
+keepIsKeep (Keep {ok = ok'} thin) z =
+  rewrite notIdUnique ok (KeepNotId ok') in Refl
+
+namespace View
+  public export
+  data View : sx `Thins` sy -> Type where
+    Id : View (id sx)
+    Drop : (thin : sx `Thins` sy) -> (0 z : a) -> View (drop thin z)
+    Keep :
+      (thin : sx `Thins` sy) ->
+      {auto 0 ok : NotId thin} ->
+      (0 z : a) ->
+      View (keep thin z)
 
-%hint
-public export
-lenPred : Len (sx :< x) -> Len sx
-lenPred (S k) = k
+  %name View view
 
 export
-Cast (Len sx) Nat where
-  cast Z = 0
-  cast (S k) = S (cast k)
-
--- Smart Constructors ----------------------------------------------------------
+view : (thin : sx `Thins` sy) -> View thin
+view Id = Id
+view (Drop thin) = Drop thin _
+view (Keep {ok} (Drop thin)) =
+  rewrite notIdUnique ok DropNotId in
+  Keep (Drop thin) _
+view (Keep {ok} (Keep {ok = ok'} thin)) =
+  rewrite notIdUnique ok (KeepNotId ok') in
+  Keep (Keep thin) _
+
+-- Indexing --------------------------------------------------------------------
 
 export
-empty : (len : Len sx) => [<] `Thins` sx
-empty {len = Z} = Empty
-empty {len = S k} = Drop empty
+index : sx `Thins` sy -> Elem x sx -> Elem x 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
-id : (len : Len sx) => sx `Thins` sx
-id {len = Z} = Empty
-id {len = S k} = Keep id
+-- Properties (more at the end)
 
-public export
-point : Len sx => Elem ty sx -> [<ty] `Thins` sx
-point Here = Keep empty
-point (There i) = Drop (point i)
+export
+indexKeepHere :
+  (thin : sx `Thins` sy) ->
+  index (keep thin z) Here = Here
+indexKeepHere Id = Refl
+indexKeepHere (Drop thin) = Refl
+indexKeepHere (Keep thin) = Refl
 
--- Operations ------------------------------------------------------------------
+export
+indexKeepThere :
+  (thin : sx `Thins` sy) ->
+  (i : Elem x sx) ->
+  index (keep thin z) (There i) = There (index thin i)
+indexKeepThere Id i = Refl
+indexKeepThere (Drop thin) i = Refl
+indexKeepThere (Keep thin) i = Refl
 
-public export
-index : sx `Thins` sy -> Elem z sx -> Elem z sy
-index (Drop thin) i = There (index thin i)
-index (Keep thin) Here = Here
-index (Keep thin) (There i) = There (index thin i)
+-- Composition -----------------------------------------------------------------
 
-public export
+export
 (.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
-Empty . thin1 = thin1
-Drop thin2 . thin1 = Drop (thin2 . thin1)
+export
+compNotId :
+  {thin2 : sy `Thins` sz} ->
+  {thin1 : sx `Thins` sy} ->
+  NotId thin2 ->
+  NotId thin1 ->
+  NotId (thin2 . thin1)
+
+Id . thin1 = thin1
+Drop thin2 . Id = Drop thin2
+Drop thin2 . thin1@(Drop _) = Drop (thin2 . thin1)
+Drop thin2 . thin1@(Keep _) = Drop (thin2 . thin1)
+Keep thin2 . Id = Keep thin2
 Keep thin2 . Drop thin1 = Drop (thin2 . thin1)
-Keep thin2 . Keep thin1 = Keep (thin2 . thin1)
+Keep {ok} thin2 . Keep {ok = ok'} thin1 = Keep {ok = compNotId ok ok'} (thin2 . thin1)
+
+compNotId DropNotId DropNotId = DropNotId
+compNotId DropNotId (KeepNotId q) = DropNotId
+compNotId (KeepNotId p) DropNotId = DropNotId
+compNotId (KeepNotId p) (KeepNotId q) = KeepNotId (compNotId p q)
+
+-- Properties (more at the end)
 
 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)
+identityRight :
+  (thin : sx `Thins` sy) ->
+  thin . id sx = thin
+identityRight Id = Refl
+identityRight (Drop thin) = Refl
+identityRight (Keep thin) = Refl
 
--- Commuting Triangles and Coverings -------------------------------------------
+export
+dropLeft :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  (0 z : a) ->
+  drop thin2 z . thin1 = drop (thin2 . thin1) z
+dropLeft thin2 Id z = sym $ cong Drop $ identityRight thin2
+dropLeft thin2 thin1@(Drop _) z = Refl
+dropLeft thin2 thin1@(Keep _) z = Refl
 
-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)
+export
+keepDrop :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  (0 z : a) ->
+  keep thin2 z . drop thin1 z = drop (thin2 . thin1) z
+keepDrop Id thin1 z = Refl
+keepDrop (Drop thin2) thin1 z = Refl
+keepDrop (Keep thin2) thin1 z = Refl
 
-public export
-data Overlap = Covers | Partitions
+export
+keepHomo :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  (0 z : a) ->
+  keep thin2 z . keep thin1 z = keep (thin2 . thin1) z
+keepHomo Id thin1 z = Refl
+keepHomo (Drop thin2) Id z = Refl
+keepHomo (Drop thin2) (Drop thin1) z = Refl
+keepHomo (Drop thin2) (Keep thin1) z = Refl
+keepHomo (Keep thin2) Id z = Refl
+keepHomo (Keep thin2) (Drop thin1) z = Refl
+keepHomo (Keep thin2) (Keep thin1) z = Refl
+
+-- Coverings and Coproducts ----------------------------------------------------
 
-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)
+export
+Covering : {a : Type} -> {sx, sy, sz : SnocList a} -> sx `Thins` sz -> sy `Thins` sz -> Type
+Covering thin1 thin2 =
+  {x : a} ->
+  (i : Elem x sz) ->
+  Either (j ** index thin1 j = i) (k ** index thin2 k = i)
 
 public export
-record Coproduct {sx, sy, sz : SnocList a} (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where
+record Coproduct {0 sx, sy : 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'
+  0 left : thin . thin1' = thin1
+  0 right : thin . thin2' = thin2
+  0 cover : Covering thin1' thin2'
+
+%name Coproduct cp
+
+coprodSym : Coproduct thin1 thin2 -> Coproduct thin2 thin1
+coprodSym cp = MkCoprod
+  cp.right
+  cp.left
+  (\i => case cp.cover i of Left x => Right x; Right x => Left x)
+
+coprodId : (thin : sx `Thins` sy) -> Coproduct Id thin
+coprodId thin = MkCoprod
+  { thin1' = Id
+  , thin2' = thin
+  , thin = Id
+  , left = Refl
+  , right = Refl
+  , cover = \i => Left (i ** Refl)
+  }
 
-export
 coprod : (thin1 : sx `Thins` sz) -> (thin2 : sy `Thins` sz) -> Coproduct thin1 thin2
-coprod Empty Empty = MkCoprod EmptyAny EmptyAny EmptyEmpty
+coprod Id thin2 = coprodId thin2
+coprod thin1@(Drop _) Id = coprodSym $ coprodId thin1
 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 ------------------------------------------------------
-
-public export
-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)
-
-public export
-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)
+  let cp = coprod thin1 thin2 in
+  MkCoprod
+    { thin1' = cp.thin1'
+    , thin2' = cp.thin2'
+    , thin = Drop cp.thin
+    , left = trans (dropLeft cp.thin cp.thin1' _) (cong Drop cp.left)
+    , right = trans (dropLeft cp.thin cp.thin2' _) (cong Drop cp.right)
+    , cover = cp.cover
+    }
+coprod (Drop thin1) (Keep {z} thin2) =
+  let cp = coprod thin1 thin2 in
+  MkCoprod
+    { thin1' = Drop cp.thin1'
+    , thin2' = keep cp.thin2' z
+    , thin = keep cp.thin z
+    , left = trans (keepDrop cp.thin cp.thin1' z) (cong Drop cp.left)
+    , right = Calc $
+      |~ keep cp.thin z . keep cp.thin2' z
+      ~~ keep (cp.thin . cp.thin2') z      ...(keepHomo cp.thin cp.thin2' z)
+      ~~ keep thin2 z                      ...(cong (\thin => keep thin z) cp.right)
+      ~~ Keep thin2                        ...(keepIsKeep thin2 z)
+    , cover = \i =>
+      case i of
+        Here => Right (Here ** indexKeepHere cp.thin2')
+        There i => case cp.cover i of
+          Left (j ** prf) => Left (j ** cong There prf)
+          Right (k ** prf) => Right (There k ** trans (indexKeepThere cp.thin2' k) (cong There prf))
+    }
+coprod thin1@(Keep _) Id = coprodSym $ coprodId thin1
+coprod (Keep {z} thin1) (Drop thin2) =
+  let cp = coprod thin1 thin2 in
+  MkCoprod
+    { thin1' = keep cp.thin1' z
+    , thin2' = Drop cp.thin2'
+    , thin = keep cp.thin z
+    , left = Calc $
+      |~ keep cp.thin z . keep cp.thin1' z
+      ~~ keep (cp.thin . cp.thin1') z      ...(keepHomo cp.thin cp.thin1' z)
+      ~~ keep thin1 z                      ...(cong (\thin => keep thin z) cp.left)
+      ~~ Keep thin1                        ...(keepIsKeep thin1 z)
+    , right = trans (keepDrop cp.thin cp.thin2' z) (cong Drop cp.right)
+    , cover = \i =>
+      case i of
+        Here => Left (Here ** indexKeepHere cp.thin1')
+        There i => case cp.cover i of
+          Left (j ** prf) => Left (There j ** trans (indexKeepThere cp.thin1' j) (cong There prf))
+          Right (k ** prf) => Right (k ** cong There prf)
+    }
+coprod (Keep {z} thin1) (Keep thin2) =
+  let cp = coprod thin1 thin2 in
+  MkCoprod
+    { thin1' = keep cp.thin1' z
+    , thin2' = keep cp.thin2' z
+    , thin = keep cp.thin z
+    , left = Calc $
+      |~ keep cp.thin z . keep cp.thin1' z
+      ~~ keep (cp.thin . cp.thin1') z      ...(keepHomo cp.thin cp.thin1' z)
+      ~~ keep thin1 z                      ...(cong (\thin => keep thin z) cp.left)
+      ~~ Keep thin1                        ...(keepIsKeep thin1 z)
+    , right = Calc $
+      |~ keep cp.thin z . keep cp.thin2' z
+      ~~ keep (cp.thin . cp.thin2') z      ...(keepHomo cp.thin cp.thin2' z)
+      ~~ keep thin2 z                      ...(cong (\thin => keep thin z) cp.right)
+      ~~ Keep thin2                        ...(keepIsKeep thin2 z)
+    , cover = \i =>
+      case i of
+        Here => Left (Here ** indexKeepHere cp.thin1')
+        There i => case cp.cover i of
+          Left (j ** prf) => Left (There j ** trans (indexKeepThere cp.thin1' j) (cong There prf))
+          Right (k ** prf) => Right (There k ** trans (indexKeepThere cp.thin2' k) (cong There prf))
+    }
 
 -- Thinned Things --------------------------------------------------------------
 
@@ -155,42 +304,25 @@ record Thinned (T : SnocList a -> Type) (sx : SnocList a) where
   thin : support `Thins` sx
 
 public export
-record OverlapPair (overlap : Overlap) (T, U : SnocList a -> Type) (sx : SnocList a) where
+record Pair (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
-
-public export
-Pair : (T, U : SnocList a -> Type) -> SnocList a -> Type
-Pair = OverlapPair Covers
+  0 cover : Covering left.thin right.thin
 
 public export
-MkPair : Thinned t sx -> Thinned u sx -> Thinned (OverlapPair Covers t u) sx
+MkPair : Thinned t sx -> Thinned u sx -> Thinned (Pair 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
-
-public export
-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
-
-public export
 map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx
 map f (value `Over` thin) = f value `Over` thin
 
 public export
-drop : Thinned t sx -> Thinned t (sx :< x)
-drop (value `Over` thin) = value `Over` Drop thin
+shift : Thinned t sx -> Thinned t (sx :< x)
+shift (value `Over` thin) = value `Over` drop thin x
 
 public export
 wkn : Thinned t sx -> sx `Thins` sy -> Thinned t sy
@@ -198,119 +330,112 @@ wkn (value `Over` thin) thin' = value `Over` thin' . thin
 
 -- Properties ------------------------------------------------------------------
 
-export
-lenUnique : (k, m : Len sx) -> k = m
-lenUnique Z Z = Refl
-lenUnique (S k) (S m) = cong S (lenUnique k m)
+-- Construction
 
 export
-emptyUnique : (thin1, thin2 : [<] `Thins` sx) -> thin1 = thin2
-emptyUnique Empty Empty = Refl
-emptyUnique (Drop thin1) (Drop thin2) = cong Drop (emptyUnique thin1 thin2)
+keepId : (0 sx : SnocList a) -> (0 x : a) -> keep (id sx) x = id (sx :< x)
+keepId sx x = Refl
+
+-- Views
 
 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)
+dropNotId : (thin : sx `Thins` sy) -> (0 y : a) -> NotId (drop thin y)
+dropNotId thin y = DropNotId
 
 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)
+keepNotId : (thin : sx `Thins` sy) -> {auto ok : NotId thin} -> (0 y : a) -> NotId (keep thin y)
+keepNotId (Drop thin) y = KeepNotId DropNotId
+keepNotId (Keep thin) {ok = KeepNotId ok} y = KeepNotId (KeepNotId ok)
+
+invertView : {0 thin : sx `Thins` sy} -> View thin -> sx `Thins` sy
+invertView Id = id sx
+invertView (Drop thin1 z) = drop thin1 z
+invertView (Keep thin1 z) = keep thin1 z
+
+invertViewCorrect : {0 thin : sx `Thins` sy} -> (view : View thin) -> invertView view = thin
+invertViewCorrect Id = Refl
+invertViewCorrect (Drop thin1 z) = Refl
+invertViewCorrect (Keep thin1 z) = Refl
+
+invertViewCorrect' :
+  {0 thin : sx `Thins` sy} ->
+  (v : View thin) ->
+  view (invertView v) = (rewrite invertViewCorrect v in v)
+invertViewCorrect' Id = Refl
+invertViewCorrect' (Drop thin z) = Refl
+invertViewCorrect' (Keep (Drop thin) {ok} z) = rewrite notIdUnique ok DropNotId in Refl
+invertViewCorrect' (Keep (Keep {ok = ok'} thin) {ok} z) =
+  rewrite notIdUnique ok (KeepNotId ok') in Refl
 
 export
-identitySquared : (len : Len sx) -> id @{len} . id @{len} = id @{len}
-identitySquared Z = Refl
-identitySquared (S k) = cong Keep (identitySquared k)
+viewUnique : {0 thin : sx `Thins` sy} -> (v1, v2 : View thin) -> v1 = v2
+viewUnique v1 v2 =
+  rewrite sym $ invertViewCorrect' v1 in
+  rewrite sym $ invertViewCorrect' v2 in
+  rewrite invertViewCorrect v1 in
+  rewrite invertViewCorrect v2 in
+  Refl
+
+-- Index
 
 export
-assoc :
-  (thin3 : sz `Thins` sw) ->
-  (thin2 : sy `Thins` sz) ->
-  (thin1 : sx `Thins` sy) ->
-  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
-assoc Empty thin2 thin1 = Refl
-assoc (Drop thin3) thin2 thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Drop thin2) thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Keep thin2) (Drop thin1) = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Keep thin2) (Keep thin1) = cong Keep (assoc thin3 thin2 thin1)
+indexId : (i : Elem x sx) -> index (id sx) i = i
+indexId i = Refl
 
 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)
+indexDrop :
+  (thin : sx `Thins` sy) ->
+  (i : Elem x sx) ->
+  index (drop thin z) i = There (index thin i)
+indexDrop thin i = Refl
 
 export
 indexHomo :
-  (thin2 : sy `Thins` sz) ->
   (thin1 : sx `Thins` sy) ->
+  (thin2 : sy `Thins` sz) ->
   (i : Elem x sx) ->
   index thin2 (index thin1 i) = index (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)
-
--- Objects
-
-export
-indexPoint : (len : Len sx) => (i : Elem x sx) -> index (point @{len} i) Here = i
-indexPoint Here = Refl
-indexPoint (There i) = cong There (indexPoint i)
-
-export
-MkTriangle :
-  (thin2 : sy `Thins` sz) ->
-  (thin1 : sx `Thins` sy) ->
-  Triangle thin2 thin1 (thin2 . thin1)
-MkTriangle Empty thin1 = EmptyAny
-MkTriangle (Drop thin2) thin1 = DropAny (MkTriangle thin2 thin1)
-MkTriangle (Keep thin2) (Drop thin1) = KeepDrop (MkTriangle thin2 thin1)
-MkTriangle (Keep thin2) (Keep thin1) = KeepKeep (MkTriangle thin2 thin1)
+indexHomo thin1 Id i = Refl
+indexHomo Id (Drop thin2) i = Refl
+indexHomo thin1@(Drop _) (Drop thin2) i = cong There $ indexHomo thin1 thin2 i
+indexHomo thin1@(Keep _) (Drop thin2) i = cong There $ indexHomo thin1 thin2 i
+indexHomo Id (Keep thin2) i = Refl
+indexHomo (Drop thin1) (Keep thin2) i = cong There $ indexHomo thin1 thin2 i
+indexHomo (Keep thin1) (Keep thin2) Here = Refl
+indexHomo (Keep thin1) (Keep thin2) (There i) = cong There $ indexHomo thin1 thin2 i
 
-export
-triangleCorrect : Triangle thin2 thin1 thin -> thin2 . thin1 = thin
-triangleCorrect EmptyAny = Refl
-triangleCorrect (DropAny t) = cong Drop (triangleCorrect t)
-triangleCorrect (KeepDrop t) = cong Drop (triangleCorrect t)
-triangleCorrect (KeepKeep t) = cong Keep (triangleCorrect t)
-
-export
-coprodEta :
-  {thin1 : sx `Thins` sz} ->
-  {thin2 : sy `Thins` sz} ->
-  (thin : sz `Thins` sw) ->
-  (cover : Covering Covers thin1 thin2) ->
-  coprod (thin . thin1) (thin . thin2) =
-  MkCoprod (MkTriangle thin thin1) (MkTriangle thin thin2) cover
-coprodEta Empty EmptyEmpty = Refl
-coprodEta (Drop thin) cover = rewrite coprodEta thin cover in Refl
-coprodEta (Keep thin) (DropKeep cover) = rewrite coprodEta thin cover in Refl
-coprodEta (Keep thin) (KeepDrop cover) = rewrite coprodEta thin cover in Refl
-coprodEta (Keep thin) (KeepKeep cover) = rewrite coprodEta thin cover in Refl
-
-export
-dropIsWkn : (len : Len sx) => (v : Thinned t sx) -> drop {x} v = wkn v (Drop $ id @{len})
-dropIsWkn (value `Over` thin) = sym $ cong ((value `Over`) . Drop) $ identityLeft thin
+-- Composition
 
 export
-wknId : (len : Len sx) => (v : Thinned t sx) -> wkn v (id @{len}) = v
-wknId (value `Over` thin) = cong (value `Over`) $ identityLeft thin
+identityLeft :
+  (thin : sx `Thins` sy) ->
+  id sy . thin = thin
+identityLeft thin = Refl
 
 export
-wknHomo :
-  (v : Thinned t sx) ->
+assoc :
+  (thin3 : sz `Thins` sw) ->
   (thin2 : sy `Thins` sz) ->
   (thin1 : sx `Thins` sy) ->
-  wkn (wkn v thin1) thin2 = wkn v (thin2 . thin1)
-wknHomo (value `Over` thin) thin2 thin1 = cong (value `Over`) $ assoc thin2 thin1 thin
-
-%hint
-export
-retractSingleton : Singleton sy -> sx `Thins` sy -> Singleton sx
-retractSingleton s Empty = s
-retractSingleton (Val (sy :< z)) (Drop thin) = retractSingleton (Val sy) thin
-retractSingleton (Val (sy :< z)) (Keep thin) = pure (:< z) <*> retractSingleton (Val sy) thin
+  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
+assoc Id thin2 thin1 = Refl
+assoc (Drop thin3) Id thin1 = Refl
+assoc (Drop thin3) thin2@(Drop _) Id = Refl
+assoc (Drop thin3) thin2@(Drop _) thin1@(Drop _) = cong Drop $ assoc thin3 thin2 thin1
+assoc (Drop thin3) thin2@(Drop _) thin1@(Keep _) = cong Drop $ assoc thin3 thin2 thin1
+assoc (Drop thin3) thin2@(Keep _) Id = Refl
+assoc (Drop thin3) thin2@(Keep _) thin1@(Drop _) = cong Drop $ assoc thin3 thin2 thin1
+assoc (Drop thin3) thin2@(Keep _) thin1@(Keep _) = cong Drop $ assoc thin3 thin2 thin1
+assoc (Keep thin3) Id thin1 = Refl
+assoc (Keep thin3) (Drop thin2) Id = Refl
+assoc (Keep thin3) (Drop thin2) thin1@(Drop _) = cong Drop $ assoc thin3 thin2 thin1
+assoc (Keep thin3) (Drop thin2) thin1@(Keep _) = 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 {ok = ok3} thin3) (Keep {ok = ok2} thin2) (Keep {ok = ok1} thin1) =
+  rewrite assoc thin3 thin2 thin1 in
+  rewrite
+    notIdUnique
+      (compNotId ok3 (compNotId ok2 ok1))
+      (rewrite assoc thin3 thin2 thin1 in compNotId (compNotId ok3 ok2) ok1) in
+  Refl
diff --git a/src/Total/Encoded/Test.idr b/src/Total/Encoded/Test.idr
new file mode 100644
index 0000000..cf5aa8e
--- /dev/null
+++ b/src/Total/Encoded/Test.idr
@@ -0,0 +1,63 @@
+module Total.Encoded.Test
+
+import Total.NormalForm
+import Total.Pretty
+import Total.Encoded.Util
+
+namespace List
+  ListC : Container
+  ListC = (Unit, 0) ::: [(N, 1)]
+
+  export
+  List : Ty
+  List = fix ListC
+
+  export
+  nil : FullTerm List [<]
+  nil = app (intro {c = ListC} Here) (app' pair [<arb, Pair.nil])
+
+  export
+  cons : FullTerm (N ~> List ~> List) [<]
+  cons = abs' (S $ S Z)
+    (\t, ts =>
+      app (lift $ intro {c = ListC} $ There Here)
+        (app' (lift pair)
+          [<t
+          , app' (lift Pair.cons) [<ts, lift Pair.nil]
+          ]))
+
+  export
+  fold : {ty : Ty} -> FullTerm ((N ~> ty ~> ty) ~> ty ~> List ~> ty) [<]
+  fold = abs' (S $ S Z)
+    (\f, z => elim
+      [ abs (drop z)
+      , abs' (S Z) (\p =>
+        app' (drop f)
+          [<app (lift $ fst {u = Vect 1 ty}) p
+          , app (lift (index {n = 1} FZ . snd {t = N})) p
+          ])
+      ])
+
+MkList : List Nat -> FullTerm List [<]
+MkList = foldr (\n, ts => app' cons [<lit n, ts]) nil
+
+sum : FullTerm (List ~> N) [<]
+sum = app' fold [<add, zero]
+
+ten : FullTerm N [<]
+ten = (app sum (MkList [1,2,3,4]))
+
+tenNf : Term [<] N
+tenNf = toTerm (normalize ten).term
+
+main : IO Builtin.Unit
+main = do
+  let
+    cases =
+      [(lit 1, id)
+      ,(lit 3, abs' (S Z) (\n => app' (lift add) [<n, n]))
+      ,(lit 2, abs' (S Z) (\n => app (lift pred) n))]
+  let t : FullTerm (N ~> N) [<] = cond cases
+  -- let t : FullTerm N [<] = app sum (MkList [1,2,3,4])
+  putDoc (group $ Doc.pretty "Input:" <+> line <+> pretty (toTerm t))
+  putDoc (group $ Doc.pretty "Normal Form:" <+> line <+> pretty (toTerm (normalize t).term))
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr
index b088e6f..0b73706 100644
--- a/src/Total/LogRel.idr
+++ b/src/Total/LogRel.idr
@@ -11,24 +11,24 @@ import Total.Term.CoDebruijn
 public export
 LogRel :
   {ctx : SnocList Ty} ->
-  (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) ->
+  (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) ->
   {ty : Ty} ->
-  (t : FullTerm ty ctx) ->
+  (t : CoTerm ty ctx) ->
   Type
 LogRel p {ty = N} t = p t
 LogRel p {ty = ty ~> ty'} t =
   (p t,
    {ctx' : SnocList Ty} ->
    (thin : ctx `Thins` ctx') ->
-   (u : FullTerm ty ctx') ->
+   (u : CoTerm ty ctx') ->
    LogRel p u ->
    LogRel p (app (wkn t thin) u))
 
 export
 escape :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   {ty : Ty} ->
-  {0 t : FullTerm ty ctx} ->
+  {0 t : CoTerm ty ctx} ->
   LogRel P t ->
   P t
 escape {ty = N} pt = pt
@@ -36,22 +36,22 @@ escape {ty = ty ~> ty'} (pt, app) = pt
 
 public export
 record PreserveHelper
-  (P : {ctx, ty : _} -> FullTerm ty ctx -> Type)
-  (R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type) where
+  (P : {ctx, ty : _} -> CoTerm ty ctx -> Type)
+  (R : {ctx, ty : _} -> CoTerm ty ctx -> CoTerm ty ctx -> Type) where
   constructor MkPresHelper
   0 app :
     {ctx : SnocList Ty} ->
     {ty, ty' : Ty} ->
-    (t, u : FullTerm (ty ~> ty') ctx) ->
+    (t, u : CoTerm (ty ~> ty') ctx) ->
     {ctx' : SnocList Ty} ->
     (thin : ctx `Thins` ctx') ->
-    (v : FullTerm ty ctx') ->
+    (v : CoTerm ty ctx') ->
     R t u ->
     R (app (wkn t thin) v) (app (wkn u thin) v)
   pres :
     {0 ctx : SnocList Ty} ->
     {ty : Ty} ->
-    {0 t, u : FullTerm ty ctx} ->
+    {0 t, u : CoTerm ty ctx} ->
     P t ->
     (0 _ : R t u) ->
     P u
@@ -60,25 +60,26 @@ record PreserveHelper
 
 export
 backStepHelper :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  (forall ctx, ty. {0 t, u : FullTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u) ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
+  (forall ctx, ty. {0 t, u : CoTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u) ->
   PreserveHelper P (flip (>) `on` CoDebruijn.toTerm)
 backStepHelper pres =
   MkPresHelper
-    (\t, u, thin, v, step =>
-      rewrite toTermApp (wkn u thin) v in
+    (\t, u, thin, v, step => ?appStep
+     {- rewrite toTermApp (wkn u thin) v in
       rewrite toTermApp (wkn t thin) v in
       rewrite sym $ wknToTerm t thin in
       rewrite sym $ wknToTerm u thin in
-      AppCong1 (wknStep step))
+      AppCong1 (wknStep step)-}
+      )
     pres
 
 export
 preserve :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  {0 R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
+  {0 R : {ctx, ty : _} -> CoTerm ty ctx -> CoTerm ty ctx -> Type} ->
   {ty : Ty} ->
-  {0 t, u : FullTerm ty ctx} ->
+  {0 t, u : CoTerm ty ctx} ->
   PreserveHelper P R ->
   LogRel P t ->
   (0 _ : R t u) ->
@@ -87,12 +88,12 @@ preserve help {ty = N} pt prf = help.pres pt prf
 preserve help {ty = ty ~> ty'} (pt, app) prf =
   (help.pres pt prf, \thin, v, rel => preserve help (app thin v rel) (help.app _ _ thin v prf))
 
-data AllLogRel : (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> CoTerms ctx ctx' -> Type where
-  Lin :
-    {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-    AllLogRel P [<]
+data AllLogRel : (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) -> Subst CoTerm ctx ctx' -> Type where
+  Base :
+    {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
+    AllLogRel P (Base thin)
   (:<) :
-    {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+    {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
     AllLogRel P sub ->
     LogRel P t ->
     AllLogRel P (sub :< t)
@@ -100,57 +101,55 @@ data AllLogRel : (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> CoTerms ctx c
 %name AllLogRel allRels
 
 index :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   ((i : Elem ty ctx') -> LogRel P (var i)) ->
-  {sub : CoTerms ctx ctx'} ->
+  {sub : Subst CoTerm ctx ctx'} ->
   AllLogRel P sub ->
   (i : Elem ty ctx) ->
   LogRel P (index sub i)
+index f Base i = f (index _ i)
 index f (allRels :< rel) Here = rel
 index f (allRels :< rel) (There i) = index f allRels i
 
 restrict :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  {0 sub : CoTerms ctx' ctx''} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
+  {0 sub : Subst CoTerm ctx' ctx''} ->
   AllLogRel P sub ->
   (thin : ctx `Thins` ctx') ->
   AllLogRel P (restrict sub thin)
-restrict [<] Empty = [<]
-restrict (allRels :< rel) (Drop thin) = restrict allRels thin
-restrict (allRels :< rel) (Keep thin) = restrict allRels thin :< rel
 
 Valid :
-  (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) ->
+  (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) ->
   {ctx : SnocList Ty} ->
   {ty : Ty} ->
-  (t : FullTerm ty ctx) ->
+  (t : CoTerm ty ctx) ->
   Type
 Valid p t =
   {ctx' : SnocList Ty} ->
-  (sub : CoTerms ctx ctx') ->
+  (sub : Subst CoTerm ctx ctx') ->
   (allRel : AllLogRel p sub) ->
   LogRel p (subst t sub)
 
 public export
-record ValidHelper (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) where
+record ValidHelper (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) where
   constructor MkValidHelper
-  var : forall ctx. Len ctx => {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (var i)
-  abs : forall ctx, ty. {ty' : Ty} -> {0 t : FullTerm ty' (ctx :< ty)} -> LogRel P t -> P (abs t)
-  zero : forall ctx. Len ctx => P {ctx} zero
-  suc : forall ctx. {0 t : FullTerm N ctx} -> P t -> P (suc t)
+  var : forall ctx. {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (var i)
+  abs : forall ctx, ty. {ty' : Ty} -> {0 t : CoTerm ty' (ctx :< ty)} -> LogRel P t -> P (abs t)
+  zero : forall ctx. P {ctx} zero
+  suc : forall ctx. {0 t : CoTerm N ctx} -> P t -> P (suc t)
   rec :
     {ctx : SnocList Ty} ->
     {ty : Ty} ->
-    {0 t : FullTerm N ctx} ->
-    {u : FullTerm ty ctx} ->
-    {v : FullTerm (ty ~> ty) ctx} ->
+    {0 t : CoTerm N ctx} ->
+    {u : CoTerm ty ctx} ->
+    {v : CoTerm (ty ~> ty) ctx} ->
     LogRel P t ->
     LogRel P u ->
     LogRel P v ->
     LogRel P (rec t u v)
-  step : forall ctx, ty. {0 t, u : FullTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u
+  step : forall ctx, ty. {0 t, u : CoTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u
   wkn : forall ctx, ctx', ty.
-    {0 t : FullTerm ty ctx} ->
+    {0 t : CoTerm ty ctx} ->
     P t ->
     (thin : ctx `Thins` ctx') ->
     P (wkn t thin)
@@ -158,101 +157,109 @@ record ValidHelper (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) where
 %name ValidHelper help
 
 wknRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   ValidHelper P ->
   {ty : Ty} ->
-  {0 t : FullTerm ty ctx} ->
+  {0 t : CoTerm ty ctx} ->
   LogRel P t ->
   (thin : ctx `Thins` ctx') ->
   LogRel P (wkn t thin)
 wknRel help {ty = N} pt thin = help.wkn pt thin
 wknRel help {ty = ty ~> ty'} (pt, app) thin =
   ( help.wkn pt thin
-  , \thin', u, rel =>
-    rewrite wknHomo t thin' thin in
-    app (thin' . thin) u rel
+  , \thin', u, rel => ?appURel
+    -- rewrite wknHomo t thin' thin in
+    -- app (thin' . thin) u rel
   )
 
 wknAllRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   ValidHelper P ->
   {ctx : SnocList Ty} ->
-  {sub : CoTerms ctx ctx'} ->
+  {sub : Subst CoTerm ctx ctx'} ->
   AllLogRel P sub ->
   (thin : ctx' `Thins` ctx'') ->
-  AllLogRel P (wknAll sub thin)
-wknAllRel help [<] thin = [<]
+  AllLogRel P (wkn sub thin)
+wknAllRel help Base thin = Base
 wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin
 
 shiftRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   ValidHelper P ->
   {ctx, ctx' : SnocList Ty} ->
-  {sub : CoTerms ctx ctx'} ->
+  {sub : Subst CoTerm ctx ctx'} ->
   AllLogRel P sub ->
-  AllLogRel P (shift {ty} sub)
-shiftRel help [<] = [<]
+  AllLogRel P (shift sub)
+shiftRel help Base = Base
 shiftRel help (allRels :< rel) =
   shiftRel help allRels :<
-  replace {p = LogRel P} (sym $ dropIsWkn _) (wknRel help rel (Drop id))
+  ?shift1
+  -- replace {p = LogRel P} (sym $ dropIsWkn _) (wknRel help rel (Drop id))
 
 liftRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   ValidHelper P ->
   {ctx, ctx' : SnocList Ty} ->
   {ty : Ty} ->
-  {sub : CoTerms ctx ctx'} ->
+  {sub : Subst CoTerm ctx ctx'} ->
   AllLogRel P sub ->
-  AllLogRel P (lift {ty} sub)
+  AllLogRel P (lift {z = ty} sub)
 liftRel help allRels = shiftRel help allRels :< help.var Here
 
-absValid :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  ValidHelper P ->
-  {ctx : SnocList Ty} ->
-  {ty, ty' : Ty} ->
-  (t : CoTerm ty' (ctx ++ used)) ->
-  (thin : used `Thins` [<ty]) ->
-  (valid : {ctx' : SnocList Ty} ->
-    (sub : CoTerms (ctx ++ used) ctx') ->
-    AllLogRel P sub ->
-    LogRel P (subst' t sub)) ->
-  {ctx' : SnocList Ty} ->
-  (sub : CoTerms ctx ctx') ->
-  AllLogRel P sub ->
-  LogRel P (subst' (Abs (MakeBound t thin)) sub)
-absValid help t (Drop Empty) valid sub allRels =
-  ( help.abs (valid (shift sub) (shiftRel help allRels))
-  , \thin, u, rel =>
-    preserve
-      (backStepHelper help.step)
-      (valid (wknAll sub thin) (wknAllRel help allRels thin))
-      ?betaStep
-  )
-absValid help t (Keep Empty) valid sub allRels =
-  ( help.abs (valid (lift sub) (liftRel help allRels))
-  , \thin, u, rel =>
-    preserve (backStepHelper help.step)
-      (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel))
-      ?betaStep'
-  )
+-- absValid :
+--   {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
+--   ValidHelper P ->
+--   {ctx : SnocList Ty} ->
+--   {ty, ty' : Ty} ->
+--   (t : FullTerm ty' (ctx ++ used)) ->
+--   (thin : used `Thins` [<ty]) ->
+--   (valid : {ctx' : SnocList Ty} ->
+--     (sub : Subst CoTerm (ctx ++ used) ctx') ->
+--     AllLogRel P sub ->
+--     LogRel P (subst' t sub)) ->
+--   {ctx' : SnocList Ty} ->
+--   (sub : Subst CoTerm ctx ctx') ->
+--   AllLogRel P sub ->
+--   LogRel P (subst' (Abs (MakeBound t thin)) sub)
+-- absValid help t (Drop Empty) valid sub allRels =
+--   ( help.abs (valid (shift sub) (shiftRel help allRels))
+--   , \thin, u, rel =>
+--     preserve
+--       (backStepHelper help.step)
+--       (valid (wkn sub thin) (wknRel help allRels thin))
+--       ?betaStep
+--   )
+-- absValid help t (Keep Empty) valid sub allRels =
+--   ( help.abs (valid (lift sub) (liftRel help allRels))
+--   , \thin, u, rel =>
+--     preserve (backStepHelper help.step)
+--       (valid (wkn sub thin :< u) (wknRel help allRels thin :< rel))
+--       ?betaStep'
+--   )
+
+%hint
+retractSingleton : Singleton ctx' -> ctx `Thins` ctx' -> Singleton ctx
+retractSingleton v Id = v
+retractSingleton v Empty = Val [<]
+retractSingleton (Val (ctx' :< ty)) (Drop thin) = retractSingleton (Val ctx') thin
+retractSingleton (Val (ctx' :< ty)) (Keep thin) = pure (:< ty) <*> retractSingleton (Val ctx') thin
 
 export
 allValid :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   ValidHelper P ->
   (s : Singleton ctx) =>
   {ty : Ty} ->
-  (t : FullTerm ty ctx) ->
+  (t : CoTerm ty ctx) ->
   Valid P t
 allValid' :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   ValidHelper P ->
   (s : Singleton ctx) =>
   {ty : Ty} ->
-  (t : CoTerm ty ctx) ->
+  (t : FullTerm ty ctx) ->
   {ctx' : SnocList Ty} ->
-  (sub : CoTerms ctx ctx') ->
+  (sub : Subst CoTerm ctx ctx') ->
   AllLogRel P sub ->
   LogRel P (subst' t sub)
 
@@ -260,14 +267,17 @@ allValid help (t `Over` thin) sub allRels =
   allValid' help t (restrict sub thin) (restrict allRels thin)
 
 allValid' help Var sub allRels = index help.var allRels Here
-allValid' help {s = Val ctx} (Abs {ty, ty'} (MakeBound t thin)) sub allRels =
-  let s' = [| Val ctx ++ retractSingleton (Val [<ty]) thin |] in
-  absValid help t thin (allValid' help t) sub allRels
+allValid' help {s = Val ctx} (Const {ty, ty'} t) sub allRels =
+  ?constValid
+allValid' help {s = Val ctx} (Abs {ty, ty'} t) sub allRels =
+  -- let s' = [| Val ctx ++ retractSingleton (Val [<ty]) thin |] in
+  ?absValid
 allValid' help (App (MakePair 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
+  ?appValid
+  -- rewrite sym $ wknId (subst t sub) in
+  -- app id (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
@@ -284,7 +294,7 @@ allValid' help (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub allRels =
 -- --   (let
 -- --       rec =
 -- --         valid
--- --           (wknAll sub (Drop id) :< Var Here)
+-- --           (wkn sub (Drop id) :< Var Here)
 -- --           (wknAllRel help allRels (Drop id) :< help.var Here)
 -- --     in
 -- --       help.abs rec
@@ -292,28 +302,28 @@ allValid' help (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub allRels =
 -- --     let
 -- --       eq :
 -- --         (subst
--- --           (wkn (subst t (wknAll sub (Drop Thinning.id) :< Var Here)) (Keep thin))
+-- --           (wkn (subst t (wkn sub (Drop Thinning.id) :< Var Here)) (Keep thin))
 -- --           (Base Thinning.id :< 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)) . (:< 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 (wkn (subst t (wkn sub (Drop id) :< Var Here)) (Keep thin)) (Base id :< u)
+-- --           ~~ subst (subst t (wkn sub (Drop id) :< Var Here)) (restrict (Base id :< u) (Keep thin))
+-- --             ...(substWkn (subst t (wkn sub (Drop id) :< Var Here)) (Keep thin) (Base id :< u))
+-- --           ~~ subst (subst t (wkn sub (Drop id) :< Var Here)) (Base thin :< u)
+-- --             ...(cong (subst (subst t (wkn sub (Drop id) :< Var Here)) . (:< u) . Base) $ identityLeft thin)
+-- --           ~~ subst t ((Base thin :< u) . wkn sub (Drop id) :< u)
+-- --             ...(substHomo t (wkn 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)
+-- --           ~~ subst t (wkn 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))
+-- --         (valid (wkn sub thin :< u) (wknRel help allRels thin :< rel))
 -- --         (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)}
 -- --           eq
 -- --           (AppBeta (length _)))
@@ -333,23 +343,25 @@ allValid' help (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub allRels =
 -- --   let relv = allValid help v sub allRels in
 -- --   help.rec relt relu relv
 
-idRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  {ctx : SnocList Ty} ->
-  ValidHelper P ->
-  AllLogRel P {ctx} (Base Thinning.id)
-idRel help {ctx = [<]} = [<]
-idRel help {ctx = ctx :< ty} = liftRel help (idRel help)
+-- idRel :
+--   {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
+--   {ctx : SnocList Ty} ->
+--   ValidHelper P ->
+--   AllLogRel P {ctx} (Base Thinning.id)
+-- idRel help {ctx = [<]} = [<]
+-- idRel help {ctx = ctx :< ty} = liftRel help (idRel help)
 
 export
 allRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} ->
   {ctx : SnocList Ty} ->
   {ty : Ty} ->
   ValidHelper P ->
-  (t : FullTerm ty ctx) ->
+  (t : CoTerm ty ctx) ->
   P t
 allRel help t =
-  rewrite sym $ substId t in
-  escape {P} $
-  allValid help @{Val ctx} t (Base id) (idRel help)
+  let rel = allValid help t (Base Id) Base in
+  ?allRel_rhs
+  -- rewrite sym $ substId t in
+  -- escape {P} $
+  -- allValid help @{Val ctx} t Base (idRel help)
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
index a7aba57..c3f16cf 100644
--- a/src/Total/NormalForm.idr
+++ b/src/Total/NormalForm.idr
@@ -29,7 +29,8 @@ data Neutral' where
 
 data Normal' where
   Ntrl : Neutral' t -> Normal' t
-  Abs : Normal' t -> Normal' (Abs (MakeBound t thin))
+  Const : Normal' t -> Normal' (Const t)
+  Abs : Normal' t -> Normal' (Abs t)
   Zero : Normal' Zero
   Suc : Normal' t -> Normal' (Suc t)
 
@@ -119,7 +120,7 @@ recNf'' Zero thin n relU relV =
   backStepsRel relU [<?recZero]
 recNf'' (Suc t) thin n relU relV =
   let rec = recNf'' t thin (invSuc n) relU relV in
-  backStepsRel (snd relV id _ rec) [<?recSuc]
+  backStepsRel (snd relV Id _ rec) [<?recSuc]
 recNf'' t@Var thin n relU relV =
   let 0 neT = WrapNe {thin} Var in
   let nfU = escape relU in
diff --git a/src/Total/Pretty.idr b/src/Total/Pretty.idr
index eade721..aa467d0 100644
--- a/src/Total/Pretty.idr
+++ b/src/Total/Pretty.idr
@@ -47,7 +47,7 @@ appPrec = App
 parameters (names : Stream String)
   export
   prettyTerm : Len ctx -> Prec -> Term ctx ty -> Doc Syntax
-  prettyTerm len d (Var i) = bound (pretty $ index (minus (cast len) (S $ elemToNat i)) names)
+  prettyTerm len d (Var i) = bound (pretty $ index (minus (lenToNat len) (S $ elemToNat i)) names)
   prettyTerm len d (Abs t) =
     let Evidence _ (len, t') = getLamNames (S len) t in
     parenthesise (d > startPrec) $ group $ align $ hang 2 $
@@ -73,7 +73,7 @@ parameters (names : Stream String)
       bound (pretty $ index offset names) <+> comma <++> prettyBindings' (S offset) (S k)
 
     prettyBindings : Len ctx' -> Doc Syntax
-    prettyBindings k = prettyBindings' (cast len) (minus (cast k) (cast len))
+    prettyBindings k = prettyBindings' (lenToNat len) (minus (lenToNat k) (lenToNat len))
   prettyTerm len d app@(App t u) =
     let (f, ts) = getSpline t [prettyArg u] in
     parenthesise (d >= appPrec) $ group $ align $ hang 2 $
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index a424515..4566724 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -4,13 +4,11 @@ import Syntax.PreorderReasoning
 import Total.Term
 
 public export
-data (>) : Term ctx ty -> Term ctx ty -> Type where
+data (>) : Term ty ctx -> Term ty ctx -> 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 :
-    (0 len : Len ctx) ->
-    App (Abs t) u > subst t (Base (id @{len}) :< u)
+  AppBeta : App (Abs t) u > subst t (Base Id :< 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
@@ -21,7 +19,7 @@ data (>) : Term ctx ty -> Term ctx ty -> Type where
 %name Reduction.(>) step
 
 public export
-data (>=) : Term ctx ty -> Term ctx ty -> Type where
+data (>=) : Term ty ctx -> Term ty ctx -> Type where
   Lin : t >= t
   (:<) : t >= u -> u > v -> t >= v
 
@@ -70,37 +68,27 @@ RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step
 -- Properties ------------------------------------------------------------------
 
 lemma :
-  (t : Term (ctx :< ty) ty') ->
+  (t : Term ty' (ctx :< ty)) ->
   (thin : ctx `Thins` ctx') ->
-  (u : Term ctx ty) ->
-  subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) =
-  wkn (subst t (Base Thinning.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 (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 @{length ctx}) :< u) thin)
+  (u : Term ty ctx) ->
+  wkn (subst t (Base Id :< u)) thin =
+  subst (wkn t (Keep thin)) (Base Id :< wkn u thin)
+lemma t thin u = Calc $
+  |~ wkn (subst t (Base Id :< u)) thin
+  ~~ subst t (wkn (Base Id :< u) thin)                      ...(wknSubst t (Base Id :< u) thin)
+  ~~ subst t (Base (thin . Id) :< wkn u thin)               ...(Refl)
+  ~~ subst t (Base thin :< wkn u thin)                      ...(substCong t (Base (identityRight thin) :< Refl))
+  ~~ subst t (Base (Id . thin) :< wkn u thin)               ...(Refl)
+  ~~ subst t (restrict (Base Id) thin :< wkn u thin)        ...(substCong t (restrictBase Id thin :< Refl))
+  ~~ subst t (restrict (Base Id :< wkn u thin) (Keep thin)) ...(Refl)
+  ~~ subst (wkn t (Keep thin)) (Base Id :< wkn u thin)      ..<(substWkn t (Base Id :< wkn u thin) (Keep 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 len {ctx, t, u}) {thin} =
-  let
-    0 eq :
-      (subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) =
-       wkn (subst t (Base (id @{len}) :< u)) thin)
-    eq = rewrite lenUnique len (length ctx) in lemma t thin u
-  in
-    rewrite sym eq in
-    AppBeta _
+wknStep (AppBeta {t, u}) {thin} = rewrite lemma 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 fead586..2710ad3 100644
--- a/src/Total/Syntax.idr
+++ b/src/Total/Syntax.idr
@@ -11,34 +11,42 @@ infixr 20 ~>*
 infixl 9 .~, .*
 
 public export
+data Len : SnocList a -> Type where
+  Z : Len [<]
+  S : Len sx -> Len (sx :< x)
+
+%name Len k
+
+export
+lenToNat : Len sx -> Nat
+lenToNat Z = 0
+lenToNat (S k) = S (lenToNat k)
+
+public export
 (~>*) : SnocList Ty -> Ty -> Ty
 tys ~>* ty = foldr (~>) ty tys
 
 public export
-0 Fun : {sx : SnocList a} -> Len sx -> (a -> Type) -> Type -> Type
-Fun Z arg ret = ret
-Fun (S {x = ty} k) arg ret = Fun k arg (arg ty -> ret)
-
-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 sx) ->
-  (forall x. p x -> q x) ->
-  Fun k q ret ->
-  Fun k p ret
-before Z f x = x
-before (S k) f x = before k f (after k (. f) x)
+0 Fun : (sx : SnocList a) -> (a -> Type) -> Type -> Type
+Fun [<] p ret = ret
+Fun (sx :< x) p ret = Fun sx p (p x -> ret)
+
+after : Len sx -> (r -> s) -> Fun sx p r -> Fun sx p s
+after Z f = f
+after (S k) f = after k (f .)
+
+before : Len sx -> (forall x. p x -> q x) -> Fun sx q ret -> Fun sx p ret
+before Z f = id
+before (S k) f = before k f . after k (. f)
 
 export
-lit : Len ctx => Nat -> FullTerm N ctx
-lit 0 = Zero `Over` empty
+lit : Nat -> FullTerm N ctx
+lit 0 = Zero `Over` Empty
 lit (S n) = suc (lit n)
 
 absHelper :
-  (k : Len tys) ->
-  Fun k (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  Len tys ->
+  Fun tys (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
   FullTerm (tys ~>* ty) ctx
 absHelper Z x = x
 absHelper (S k) x =
@@ -48,11 +56,10 @@ absHelper (S k) x =
 
 export
 abs' :
-  (len : Len ctx) =>
-  (k : Len tys) ->
-  Fun k (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  Len tys ->
+  Fun tys (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
   FullTerm (tys ~>* ty) ctx
-abs' k = absHelper k . before k (var @{lenAppend len k})
+abs' k = absHelper k . before k var
 
 export
 app' :
@@ -97,7 +104,6 @@ app' t (us :< u) = app (app' t us) u
 
 export
 (.) :
-  Len ctx =>
   {ty, ty' : Ty} ->
   FullTerm (ty' ~> ty'') ctx ->
   FullTerm (ty ~> ty') ctx ->
@@ -106,7 +112,6 @@ t . u = abs' (S Z) (\x => app (drop t) (app (drop u) x))
 
 export
 (.*) :
-  Len ctx =>
   {ty : Ty} ->
   {tys : SnocList Ty} ->
   FullTerm (ty ~> ty') ctx ->
@@ -116,13 +121,9 @@ export
 (.*) {tys = tys :< ty''} t u = abs' (S Z) (\f => drop t . f) .*  u
 
 export
-lift : Len ctx => FullTerm ty [<] -> FullTerm ty ctx
-lift t = wkn t empty
-
-export
-id' : CoTerm (ty ~> ty) [<]
-id' = Abs (MakeBound Var (Keep Empty))
+lift : FullTerm ty [<] -> FullTerm ty ctx
+lift t = wkn t Empty
 
 export
 id : FullTerm (ty ~> ty) [<]
-id = id' `Over` empty
+id = Abs Var `Over` Empty
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 129662a..7d6fba0 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -1,13 +1,19 @@
 module Total.Term
 
+import Control.Relation
 import public Data.SnocList.Elem
+import public Subst
 import public Thinning
+
 import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Generic
 
 %prefix_record_projections off
 
 infixr 10 ~>
 
+-- Types -----------------------------------------------------------------------
+
 public export
 data Ty : Type where
   N : Ty
@@ -15,64 +21,48 @@ data Ty : Type where
 
 %name Ty ty
 
+-- Definition ------------------------------------------------------------------
+
 public export
-data Term : SnocList Ty -> Ty -> Type where
-  Var : (i : Elem ty ctx) -> Term ctx ty
-  Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty')
-  App : {ty : Ty} -> Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty'
-  Zero : Term ctx N
-  Suc : Term ctx N -> Term ctx N
-  Rec : Term ctx N -> Term ctx ty -> Term ctx (ty ~> ty) -> Term ctx ty
+data Term : Ty -> SnocList Ty -> Type where
+  Var : (i : Elem ty ctx) -> Term ty ctx
+  Abs : Term ty' (ctx :< ty) -> Term (ty ~> ty') ctx
+  App : {ty : Ty} -> Term (ty ~> ty') ctx -> Term ty ctx -> Term ty' ctx
+  Zero : Term N ctx
+  Suc : Term N ctx -> Term N ctx
+  Rec : Term N ctx -> Term ty ctx -> Term (ty ~> ty) ctx -> Term ty ctx
 
 %name Term t, u, v
 
-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 (App t u) thin = App (wkn t thin) (wkn u thin)
-wkn Zero thin = Zero
-wkn (Suc t) thin = Suc (wkn t thin)
-wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin)
+-- Raw Interfaces --------------------------------------------------------------
 
-public export
-data Terms : SnocList Ty -> SnocList Ty -> Type where
-  Base : ctx `Thins` ctx' -> Terms ctx' ctx
-  (:<) : Terms ctx' ctx -> Term ctx' ty -> Terms ctx' (ctx :< ty)
+export
+Point Ty Term where
+  point = Var
 
-%name Terms sub
+export
+Weaken Ty Term where
+  wkn (Var i) thin = Var (index thin i)
+  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)
+  wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin)
 
-public export
-index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty
-index (Base thin) i = Var (index thin i)
-index (sub :< t) Here = t
-index (sub :< t) (There i) = index sub i
+export
+PointWeaken Ty Term where
 
-public export
-wknAll : Terms ctx' ctx -> ctx' `Thins` ctx'' -> Terms ctx'' ctx
-wknAll (Base thin') thin = Base (thin . thin')
-wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
+-- Substitution ----------------------------------------------------------------
 
 public export
-subst : Len ctx' => Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
+subst : Term ty ctx -> Subst Term ctx ctx' -> Term ty ctx'
 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 $ lift sub)
 subst (App t u) sub = App (subst t sub) (subst u sub)
 subst Zero sub = Zero
 subst (Suc t) sub = Suc (subst t sub)
 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) (Drop thin) = restrict sub thin
-restrict (sub :< t) (Keep thin) = restrict sub thin :< t
-
-public export
-(.) : Len ctx'' => Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx
-sub2 . (Base thin) = restrict sub2 thin
-sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2
-
 -- Properties ------------------------------------------------------------------
 
 -- Utilities
@@ -84,106 +74,63 @@ cong3 f Refl Refl Refl = Refl
 -- Weakening
 
 export
-wknHomo :
-  (t : Term ctx ty) ->
-  (thin1 : ctx `Thins` ctx') ->
-  (thin2 : ctx' `Thins` ctx'') ->
-  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
-wknHomo (Var i) thin1 thin2 =
-  cong Var (indexHomo thin2 thin1 i)
-wknHomo (Abs t) thin1 thin2 =
-  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 =
-  Refl
-wknHomo (Suc t) thin1 thin2 =
-  cong Suc (wknHomo t thin1 thin2)
-wknHomo (Rec t u v) thin1 thin2 =
-  cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2)
+FullWeaken Ty Term where
+  shiftIsWkn t = Refl
+
+  wknId (Var i) = cong Var $ indexId i
+  wknId (Abs t) = cong Abs $ trans (cong (wkn t) (keepId _ _)) (wknId t)
+  wknId (App t u) = cong2 App (wknId t) (wknId u)
+  wknId Zero = Refl
+  wknId (Suc t) = cong Suc (wknId t)
+  wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v)
+
+  wknHomo (Var i) thin1 thin2 = cong Var $ indexHomo thin1 thin2 i
+  wknHomo (Abs t) thin1 thin2 =
+    cong Abs $
+      trans
+        (wknHomo t (keep thin1 _) (keep thin2 _))
+        (cong (wkn t) $ keepHomo thin2 thin1 _)
+  wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
+  wknHomo Zero thin1 thin2 = Refl
+  wknHomo (Suc t) thin1 thin2 = cong Suc (wknHomo t thin1 thin2)
+  wknHomo (Rec t u v) thin1 thin2 =
+    cong3 Rec
+      (wknHomo t thin1 thin2)
+      (wknHomo u thin1 thin2)
+      (wknHomo v thin1 thin2)
 
 export
-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
-wknId (Suc t) = cong Suc (wknId t)
-wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v)
-
-indexWknAll :
-  (sub : Terms ctx' ctx) ->
-  (thin : ctx' `Thins` ctx'') ->
-  (i : Elem ty ctx) ->
-  index (wknAll sub thin) i = wkn (index sub i) thin
-indexWknAll (Base thin') thin i = sym $ cong Var $ indexHomo thin thin' i
-indexWknAll (sub :< t) thin Here = Refl
-indexWknAll (sub :< t) thin (There i) = indexWknAll sub thin i
-
-wknAllHomo :
-  (sub : Terms ctx ctx''') ->
-  (thin1 : ctx `Thins` ctx') ->
-  (thin2 : ctx' `Thins` ctx'') ->
-  wknAll (wknAll sub thin1) thin2 = wknAll sub (thin2 . thin1)
-wknAllHomo (Base thin) thin1 thin2 = cong Base (assoc thin2 thin1 thin)
-wknAllHomo (sub :< t) thin1 thin2 = cong2 (:<) (wknAllHomo sub thin1 thin2) (wknHomo t thin1 thin2)
-
--- Restrict
-
-indexRestrict :
-  (thin : ctx `Thins` ctx') ->
-  (sub : Terms ctx'' ctx') ->
-  (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 (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 : (len : Len ctx) => (sub : Terms ctx' ctx) -> restrict sub (id @{len}) = sub
-restrictId (Base thin) = cong Base (identityRight thin)
-restrictId {len = S k} (sub :< t) = cong (:< t) (restrictId sub)
-
-restrictHomo :
-  (sub : Terms ctx ctx''') ->
-  (thin1 : ctx'' `Thins` ctx''') ->
-  (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) (Drop thin1) thin2 = restrictHomo sub thin1 thin2
-restrictHomo (sub :< t) (Keep thin1) (Drop thin2) = restrictHomo sub thin1 thin2
-restrictHomo (sub :< t) (Keep thin1) (Keep thin2) = cong (:< t) $ restrictHomo sub thin1 thin2
-
-wknAllRestrict :
-  (thin1 : ctx `Thins` ctx') ->
-  (sub : Terms ctx'' ctx') ->
-  (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 (Drop thin) (sub :< t) thin2 = wknAllRestrict thin sub thin2
-wknAllRestrict (Keep thin) (sub :< t) thin2 = cong (:< wkn t thin2) (wknAllRestrict thin sub thin2)
+FullPointWeaken Ty Term where
+  wknPoint i thin = Refl
 
 -- Substitution & Weakening
 
 export
+substCong :
+  (t : Term ty ctx) ->
+  {0 sub1, sub2 : Subst Term ctx ctx'} ->
+  Equiv sub1 sub2 ->
+  subst t sub1 = subst t sub2
+substCong (Var i) e = e.equiv i
+substCong (Abs t) e = cong Abs $ substCong t (liftCong e)
+substCong (App t u) e = cong2 App (substCong t e) (substCong u e)
+substCong Zero e = Refl
+substCong (Suc t) e = cong Suc (substCong t e)
+substCong (Rec t u v) e = cong3 Rec (substCong t e) (substCong u e) (substCong v e)
+
+export
 wknSubst :
-  (t : Term ctx ty) ->
-  (sub : Terms ctx' ctx) ->
+  (t : Term ty ctx) ->
+  (sub : Subst Term ctx ctx') ->
   (thin : ctx' `Thins` ctx'') ->
-  wkn (subst t sub) thin = subst t (wknAll sub thin)
+  wkn (subst t sub) thin = subst t (wkn sub thin)
 wknSubst (Var i) sub thin =
-  sym (indexWknAll sub thin i)
-wknSubst (Abs t) sub thin =
+  indexWkn sub thin i
+wknSubst (Abs {ty} t) sub thin =
   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)
-      ...(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))
+    |~ wkn (subst t (lift sub)) (keep thin ty)
+    ~~ subst t (wkn (lift sub) (keep thin ty)) ...(wknSubst t (lift sub) (keep thin _))
+    ~~ subst t (lift (wkn sub thin))           ...(substCong t (wknLift sub thin))
 wknSubst (App t u) sub thin =
   cong2 App (wknSubst t sub thin) (wknSubst u sub thin)
 wknSubst Zero sub thin =
@@ -195,163 +142,125 @@ wknSubst (Rec t u v) sub thin =
 
 export
 substWkn :
-  (t : Term ctx ty) ->
+  (t : Term ty ctx) ->
+  (sub : Subst Term ctx' ctx'') ->
   (thin : ctx `Thins` ctx') ->
-  (sub : Terms ctx'' ctx') ->
   subst (wkn t thin) sub = subst t (restrict sub thin)
-substWkn (Var i) thin sub =
-  sym (indexRestrict thin sub i)
-substWkn (Abs t) thin sub =
-  cong Abs $ Calc $
-    |~ 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 =
-  Refl
-substWkn (Suc t) thin sub =
-  cong Suc (substWkn t thin sub)
-substWkn (Rec t u v) thin sub =
-  cong3 Rec (substWkn t thin sub) (substWkn u thin sub) (substWkn 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)
-    WknAll :
-      (len : Len ctx) =>
-      Equiv sub sub' ->
-      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 = 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)
-
-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 (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)
-substCong (Rec t u v) prf = cong3 Rec (substCong t prf) (substCong u prf) (substCong v prf)
-
-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 =
-  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)
-substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin)
-
--- Substitution Composition
-
-indexComp :
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx'' ctx') ->
-  (i : Elem ty ctx) ->
-  index (sub2 . sub1) i = subst (index sub1 i) sub2
-indexComp (Base thin) sub2 i = indexRestrict thin sub2 i
-indexComp (sub1 :< t) sub2 Here = Refl
-indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i
-
-wknAllComp :
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx'' ctx') ->
-  (thin : ctx'' `Thins` ctx''') ->
-  wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin
-wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin
-wknAllComp (sub1 :< t) sub2 thin =
-  cong2 (:<)
-    (wknAllComp sub1 sub2 thin)
-    (sym $ wknSubst t sub2 thin)
-
-compDrop :
-  (sub1 : Terms ctx' ctx) ->
-  (thin : ctx' `Thins` ctx'') ->
-  (sub2 : Terms ctx''' ctx'') ->
-  sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
-compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin'
-compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2)
-
-export
-compWknAll :
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx''' ctx'') ->
-  (thin : ctx' `Thins` ctx'') ->
-  sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
-compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin'
-compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2)
-
-export
-baseComp :
-  (thin : ctx' `Thins` ctx'') ->
-  (sub : Terms ctx' ctx) ->
-  Base thin . sub = wknAll sub thin
-baseComp thin (Base thin') = Refl
-baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
-
--- Substitution
-
-export
-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 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)
-substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v)
-
-export
-substHomo :
-  (t : Term ctx ty) ->
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx'' ctx') ->
-  subst (subst t sub1) sub2 = subst t (sub2 . sub1)
-substHomo (Var i) sub1 sub2 =
-  sym $ indexComp sub1 sub2 i
-substHomo (Abs t) sub1 sub2 =
+substWkn (Var i) sub thin =
+  indexRestrict sub thin i
+substWkn (Abs t) sub thin =
   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)
-      ...(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))
-substHomo (App t u) sub1 sub2 =
-  cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2)
-substHomo Zero sub1 sub2 =
+    |~ subst (wkn t (keep thin _)) (lift sub)
+    ~~ subst t (restrict (lift sub) (keep thin _)) ...(substWkn t (lift sub) (keep thin _))
+    ~~ subst t (lift (restrict sub thin))          ...(substCong t (restrictLift sub thin))
+substWkn (App t u) sub thin =
+  cong2 App (substWkn t sub thin) (substWkn u sub thin)
+substWkn Zero sub thin =
   Refl
-substHomo (Suc t) sub1 sub2 =
-  cong Suc (substHomo t sub1 sub2)
-substHomo (Rec t u v) sub1 sub2 =
-  cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2)
+substWkn (Suc t) sub thin =
+  cong Suc (substWkn t sub thin)
+substWkn (Rec t u v) sub thin =
+  cong3 Rec (substWkn t sub thin) (substWkn u sub thin) (substWkn v sub thin)
+
+-- -- 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 =
+-- --   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)
+-- -- substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin)
+
+-- -- -- Substitution Composition
+
+-- -- indexComp :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx'' ctx') ->
+-- --   (i : Elem ty ctx) ->
+-- --   index (sub2 . sub1) i = subst (index sub1 i) sub2
+-- -- indexComp (Base thin) sub2 i = indexRestrict thin sub2 i
+-- -- indexComp (sub1 :< t) sub2 Here = Refl
+-- -- indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i
+
+-- -- wknAllComp :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx'' ctx') ->
+-- --   (thin : ctx'' `Thins` ctx''') ->
+-- --   wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin
+-- -- wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin
+-- -- wknAllComp (sub1 :< t) sub2 thin =
+-- --   cong2 (:<)
+-- --     (wknAllComp sub1 sub2 thin)
+-- --     (sym $ wknSubst t sub2 thin)
+
+-- -- compDrop :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (thin : ctx' `Thins` ctx'') ->
+-- --   (sub2 : Terms ctx''' ctx'') ->
+-- --   sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
+-- -- compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin'
+-- -- compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2)
+
+-- -- export
+-- -- compWknAll :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx''' ctx'') ->
+-- --   (thin : ctx' `Thins` ctx'') ->
+-- --   sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
+-- -- compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin'
+-- -- compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2)
+
+-- -- export
+-- -- baseComp :
+-- --   (thin : ctx' `Thins` ctx'') ->
+-- --   (sub : Terms ctx' ctx) ->
+-- --   Base thin . sub = wknAll sub thin
+-- -- baseComp thin (Base thin') = Refl
+-- -- baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
+
+-- -- -- Substitution
+
+-- -- export
+-- -- 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 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)
+-- -- substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v)
+
+-- -- export
+-- -- substHomo :
+-- --   (t : Term ctx ty) ->
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx'' ctx') ->
+-- --   subst (subst t sub1) sub2 = subst t (sub2 . sub1)
+-- -- substHomo (Var i) sub1 sub2 =
+-- --   sym $ indexComp sub1 sub2 i
+-- -- substHomo (Abs t) sub1 sub2 =
+-- --   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)
+-- --       ...(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))
+-- -- substHomo (App t u) sub1 sub2 =
+-- --   cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2)
+-- -- substHomo Zero sub1 sub2 =
+-- --   Refl
+-- -- substHomo (Suc t) sub1 sub2 =
+-- --   cong Suc (substHomo t sub1 sub2)
+-- -- substHomo (Rec t u v) sub1 sub2 =
+-- --   cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2)
diff --git a/src/Total/Term/CoDebruijn.idr b/src/Total/Term/CoDebruijn.idr
index 0efcdbb..8c8ba13 100644
--- a/src/Total/Term/CoDebruijn.idr
+++ b/src/Total/Term/CoDebruijn.idr
@@ -10,98 +10,75 @@ import Total.Term
 -- Definition ------------------------------------------------------------------
 
 public export
-data CoTerm : Ty -> SnocList Ty -> Type where
-  Var : CoTerm ty [<ty]
-  Abs : Binds [<ty] (CoTerm ty') ctx -> CoTerm (ty ~> ty') ctx
-  App : {ty : Ty} -> Pair (CoTerm (ty ~> ty')) (CoTerm ty) ctx -> CoTerm ty' ctx
-  Zero : CoTerm N [<]
-  Suc : CoTerm N ctx -> CoTerm N ctx
-  Rec : Pair (CoTerm N) (Pair (CoTerm ty) (CoTerm (ty ~> ty))) ctx -> CoTerm ty ctx
+data FullTerm : Ty -> SnocList Ty -> Type where
+  Var : FullTerm ty [<ty]
+  Const : FullTerm ty' ctx -> FullTerm (ty ~> ty') ctx
+  Abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx
+  App : {ty : Ty} -> Pair (FullTerm (ty ~> ty')) (FullTerm ty) ctx -> FullTerm ty' ctx
+  Zero : FullTerm N [<]
+  Suc : FullTerm N ctx -> FullTerm N ctx
+  Rec : Pair (FullTerm N) (Pair (FullTerm ty) (FullTerm (ty ~> ty))) ctx -> FullTerm ty ctx
 
-%name CoTerm t, u, v
+%name FullTerm t, u, v
 
 public export
-FullTerm : Ty -> SnocList Ty -> Type
-FullTerm ty ctx = Thinned (CoTerm ty) ctx
+CoTerm : Ty -> SnocList Ty -> Type
+CoTerm ty ctx = Thinned (FullTerm ty) ctx
 
 -- Smart Constructors ----------------------------------------------------------
 
 public export
-var : Len ctx => Elem ty ctx -> FullTerm ty ctx
-var i = Var `Over` point i
+var : Elem ty ctx -> CoTerm ty ctx
+var i = Var `Over` Point i
 
 public export
-abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx
-abs = map Abs . MkBound (S Z)
+abs : CoTerm ty' (ctx :< ty) -> CoTerm (ty ~> ty') ctx
+abs (t `Over` Id) = Abs t `Over` Id
+abs (t `Over` Empty) = Const t `Over` Empty
+abs (t `Over` Drop thin) = Const t `Over` thin
+abs (t `Over` Keep thin) = Abs t `Over` thin
 
 public export
-app : {ty : Ty} -> FullTerm (ty ~> ty') ctx -> FullTerm ty ctx -> FullTerm ty' ctx
+app : {ty : Ty} -> CoTerm (ty ~> ty') ctx -> CoTerm ty ctx -> CoTerm ty' ctx
 app t u = map App (MkPair t u)
 
 public export
-zero : Len ctx => FullTerm N ctx
-zero = Zero `Over` empty
+zero : CoTerm N ctx
+zero = Zero `Over` Empty
 
 public export
-suc : FullTerm N ctx -> FullTerm N ctx
+suc : CoTerm N ctx -> CoTerm N ctx
 suc = map Suc
 
 public export
-rec : FullTerm N ctx -> FullTerm ty ctx -> FullTerm (ty ~> ty) ctx -> FullTerm ty ctx
+rec : CoTerm N ctx -> CoTerm ty ctx -> CoTerm (ty ~> ty) ctx -> CoTerm ty ctx
 rec t u v = map Rec $ MkPair t (MkPair u v)
 
--- Substitutions ---------------------------------------------------------------
+-- Raw Interfaces --------------------------------------------------------------
 
-public export
-data CoTerms : SnocList Ty -> SnocList Ty -> Type where
-  Lin : CoTerms [<] ctx'
-  (:<) : CoTerms ctx ctx' -> FullTerm ty ctx' -> CoTerms (ctx :< ty) ctx'
-
-%name CoTerms sub
-
-public export
-index : CoTerms ctx ctx' -> Elem ty ctx -> FullTerm ty ctx'
-index (sub :< t) Here = t
-index (sub :< t) (There i) = index sub i
-
-public export
-wknAll : CoTerms ctx ctx' -> ctx' `Thins` ctx'' -> CoTerms ctx ctx''
-wknAll [<] thin = [<]
-wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
-
-public export
-shift : CoTerms ctx ctx' -> CoTerms ctx (ctx' :< ty)
-shift [<] = [<]
-shift (sub :< t) = shift sub :< drop t
-
-public export
-lift : Len ctx' => CoTerms ctx ctx' -> CoTerms (ctx :< ty) (ctx' :< ty)
-lift sub = shift sub :< var Here
+export
+Point Ty CoTerm where
+  point = var
 
-public export
-restrict : CoTerms ctx' ctx'' -> ctx `Thins` ctx' -> CoTerms ctx ctx''
-restrict [<] Empty = [<]
-restrict (sub :< t) (Drop thin) = restrict sub thin
-restrict (sub :< t) (Keep thin) = restrict sub thin :< t
+export
+Weaken Ty CoTerm where
+  wkn = Thinning.wkn
+  drop = Thinning.drop
 
-public export
-Base : (len : Len ctx') => ctx `Thins` ctx' -> CoTerms ctx ctx'
-Base Empty = [<]
-Base {len = S k} (Drop thin) = shift (Base thin)
-Base {len = S k} (Keep thin) = lift (Base thin)
+export PointWeaken Ty CoTerm where
 
 -- Substitution Operation ------------------------------------------------------
 
 public export
-subst : Len ctx' => FullTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
+subst : CoTerm ty ctx -> Subst CoTerm ctx ctx' -> CoTerm ty ctx'
 public export
-subst' : Len ctx' => CoTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
+subst' : FullTerm ty ctx -> Subst CoTerm ctx ctx' -> CoTerm ty ctx'
 
 subst (t `Over` thin) sub = subst' t (restrict sub thin)
 
 subst' Var sub = index sub Here
-subst' (Abs (MakeBound t (Drop Empty))) sub = abs (subst' t $ shift sub)
-subst' (Abs (MakeBound t (Keep Empty))) sub = abs (subst' t $ lift sub)
+subst' (Const t) sub = abs (drop $ subst' t sub)
+subst' (Abs t) sub = abs (subst' t $ lift sub)
 subst' (App (MakePair t u _)) sub = app (subst t sub) (subst u sub)
 subst' Zero sub = zero
 subst' (Suc t) sub = suc (subst' t sub)
@@ -110,10 +87,10 @@ subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub =
 
 -- Initiality ------------------------------------------------------------------
 
-toTerm' : CoTerm ty ctx -> ctx `Thins` ctx' -> Term ctx' ty
+toTerm' : FullTerm ty ctx -> ctx `Thins` ctx' -> Term ty ctx'
 toTerm' Var thin = Var (index thin Here)
-toTerm' (Abs (MakeBound t (Drop Empty))) thin = Abs (toTerm' t (Drop thin))
-toTerm' (Abs (MakeBound t (Keep Empty))) thin = Abs (toTerm' t (Keep thin))
+toTerm' (Const t) thin = Abs (toTerm' t (Drop thin))
+toTerm' (Abs t) thin = Abs (toTerm' t (Keep thin))
 toTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
   App (toTerm' t (thin . thin1)) (toTerm' u (thin . thin2))
 toTerm' Zero thin = Zero
@@ -130,188 +107,184 @@ toTerm'
     (toTerm' v ((thin . thin') . thin3))
 
 export
-toTerm : FullTerm ty ctx -> Term ctx ty
+toTerm : CoTerm ty ctx -> Term ty ctx
 toTerm (t `Over` thin) = toTerm' t thin
 
-public export
-toTerms : Len ctx' => CoTerms ctx ctx' -> Terms ctx' ctx
-toTerms [<] = Base empty
-toTerms (sub :< t) = toTerms sub :< toTerm t
-
 export
-Cast (FullTerm ty ctx) (Term ctx ty) where
-  cast = toTerm
-
-export
-Len ctx' => Cast (CoTerms ctx ctx') (Terms ctx' ctx) where
-  cast = toTerms
-
-export
-Len ctx => Cast (Term ctx ty) (FullTerm ty ctx) where
-  cast (Var i) = Var `Over` point i
-  cast (Abs t) = abs (cast t)
-  cast (App {ty} t u) = app {ty} (cast t) (cast u)
-  cast Zero = zero
-  cast (Suc t) = suc (cast t)
-  cast (Rec t u v) = rec (cast t) (cast u) (cast v)
+fromTerm : Term ty ctx -> CoTerm ty ctx
+fromTerm (Var i) = var i
+fromTerm (Abs t) = abs (fromTerm t)
+fromTerm (App t u) = app (fromTerm t) (fromTerm u)
+fromTerm Zero = zero
+fromTerm (Suc t) = suc (fromTerm t)
+fromTerm (Rec t u v) = rec (fromTerm t) (fromTerm u) (fromTerm v)
 
 -- Properties ------------------------------------------------------------------
 
-wknToTerm' :
-  (t : CoTerm ty ctx) ->
-  (thin : ctx `Thins` ctx') ->
-  (thin' : ctx' `Thins` ctx''') ->
-  wkn (toTerm' t thin) thin' = toTerm' t (thin' . thin)
-wknToTerm' Var thin thin' = cong Var (indexHomo thin' thin Here)
-wknToTerm' (Abs (MakeBound t (Drop Empty))) thin thin' =
-  cong Abs (wknToTerm' t (Drop thin) (Keep thin'))
-wknToTerm' (Abs (MakeBound t (Keep Empty))) thin thin' =
-  cong Abs (wknToTerm' t (Keep thin) (Keep thin'))
-wknToTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin thin' =
-  rewrite sym $ assoc thin' thin thin1 in
-  rewrite sym $ assoc thin' thin thin2 in
-  cong2 App (wknToTerm' t (thin . thin1) thin') (wknToTerm' u (thin . thin2) thin')
-wknToTerm' Zero thin thin' = Refl
-wknToTerm' (Suc t) thin thin' = cong Suc (wknToTerm' t thin thin')
-wknToTerm'
-  (Rec
-    (MakePair
-      (t `Over` thin1)
-      (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin'') _))
-  thin
-  thin' =
-  rewrite sym $ assoc thin' thin thin1 in
-  rewrite sym $ assoc (thin' . thin) thin'' thin2 in
-  rewrite sym $ assoc thin'  thin (thin'' . thin2) in
-  rewrite sym $ assoc thin thin'' thin2 in
-  rewrite sym $ assoc (thin' . thin) thin'' thin3 in
-  rewrite sym $ assoc thin'  thin (thin'' . thin3) in
-  rewrite sym $ assoc thin thin'' thin3 in
-  cong3 Rec
-    (wknToTerm' t (thin . thin1) thin')
-    (wknToTerm' u (thin . (thin'' . thin2)) thin')
-    (wknToTerm' v (thin . (thin'' . thin3)) thin')
-
-export
-wknToTerm :
-  (t : FullTerm ty ctx) ->
-  (thin : ctx `Thins` ctx') ->
-  wkn (toTerm t) thin = toTerm (wkn t thin)
-wknToTerm (t `Over` thin') thin = wknToTerm' t thin' thin
-
-export
-toTermVar : Len ctx => (i : Elem ty ctx) -> toTerm (var i) = Var i
-toTermVar i = cong Var $ indexPoint i
-
-export
-toTermApp :
-  (t : FullTerm (ty ~> ty') ctx) ->
-  (u : FullTerm ty ctx) ->
-  toTerm (app t u) = App (toTerm t) (toTerm u)
-toTermApp (t `Over` thin1) (u `Over` thin2) =
-  cong2 App
-    (cong (toTerm' t) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).left)
-    (cong (toTerm' u) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).right)
-
-indexShift :
-  (sub : CoTerms ctx ctx') ->
-  (i : Elem ty ctx) ->
-  index (shift sub) i = drop (index sub i)
-indexShift (sub :< t) Here = Refl
-indexShift (sub :< t) (There i) = indexShift sub i
-
-indexBase : (thin : [<ty] `Thins` ctx') -> index (Base thin) Here = Var `Over` thin
-indexBase (Drop thin) = trans (indexShift (Base thin) Here) (cong drop (indexBase thin))
-indexBase (Keep thin) = irrelevantEq $ cong ((Var `Over`) . Keep) $ emptyUnique empty thin
-
-restrictShift :
-  (sub : CoTerms ctx' ctx'') ->
-  (thin : ctx `Thins` ctx') ->
-  restrict (shift sub) thin = shift (restrict sub thin)
-restrictShift [<] Empty = Refl
-restrictShift (sub :< t) (Drop thin) = restrictShift sub thin
-restrictShift (sub :< t) (Keep thin) = cong (:< drop t) (restrictShift sub thin)
-
-restrictBase :
-  (thin2 : ctx' `Thins` ctx'') ->
-  (thin1 : ctx `Thins` ctx') ->
-  CoDebruijn.restrict (Base thin2) thin1 = Base (thin2 . thin1)
-restrictBase Empty Empty = Refl
-restrictBase (Drop thin2) thin1 =
-  trans
-    (restrictShift (Base thin2) thin1)
-    (cong shift $ restrictBase thin2 thin1)
-restrictBase (Keep thin2) (Drop thin1) =
-  trans
-    (restrictShift (Base thin2) thin1)
-    (cong shift $ restrictBase thin2 thin1)
-restrictBase (Keep thin2) (Keep thin1) =
-  cong (:< (Var `Over` point Here)) $
-  trans
-    (restrictShift (Base thin2) thin1)
-    (cong shift $ restrictBase thin2 thin1)
-
-substBase :
-  (t : CoTerm ty ctx) ->
-  (thin : ctx `Thins` ctx') ->
-  subst' t (Base thin) = t `Over` thin
-substBase Var thin = indexBase thin
-substBase (Abs (MakeBound t (Drop Empty))) thin =
-  Calc $
-    |~ map Abs (MkBound (S Z) (subst' t (shift $ Base thin)))
-    ~~ map Abs (MkBound (S Z) (t `Over` Drop thin))
-      ...(cong (map Abs . MkBound (S Z)) $ substBase t (Drop thin))
-    ~~ map Abs (MakeBound t (Drop Empty) `Over` thin)
-      ...(Refl)
-    ~~ (Abs (MakeBound t (Drop Empty)) `Over` thin)
-      ...(Refl)
-substBase (Abs (MakeBound t (Keep Empty))) thin = 
-  Calc $
-    |~ map Abs (MkBound (S Z) (subst' t (lift $ Base thin)))
-    ~~ map Abs (MkBound (S Z) (t `Over` Keep thin))
-      ...(cong (map Abs . MkBound (S Z)) $ substBase t (Keep thin))
-    ~~ map Abs (MakeBound t (Keep Empty) `Over` thin)
-      ...(Refl)
-    ~~ (Abs (MakeBound t (Keep Empty)) `Over` thin)
-      ...(Refl)
-substBase (App (MakePair (t `Over` thin1) (u `Over` thin2) cover)) thin =
-  rewrite restrictBase thin thin1 in
-  rewrite restrictBase thin thin2 in
-  rewrite substBase t (thin . thin1) in
-  rewrite substBase u (thin . thin2) in
-  rewrite coprodEta thin cover in
-  Refl
-substBase Zero thin = cong (Zero `Over`) $ irrelevantEq $ emptyUnique empty thin
-substBase (Suc t) thin = cong (map Suc) $ substBase t thin
-substBase
-  (Rec (MakePair
-      (t `Over` thin1)
-      (MakePair
-        (u `Over` thin2)
-        (v `Over` thin3)
-        cover'
-      `Over` thin')
-      cover))
-  thin =
-  rewrite restrictBase thin thin1 in
-  rewrite restrictBase thin thin' in
-  rewrite restrictBase (thin . thin') thin2 in
-  rewrite restrictBase (thin . thin') thin3 in
-  rewrite substBase t (thin . thin1) in
-  rewrite substBase u ((thin . thin') . thin2) in
-  rewrite substBase v ((thin . thin') . thin3) in
-  rewrite coprodEta (thin . thin') cover' in
-  rewrite coprodEta thin cover in
-  Refl
+-- Weakening
 
 export
-substId : (t : FullTerm ty ctx) -> subst t (Base Thinning.id) = t
-substId (t `Over` thin) =
-  Calc $
-    |~ subst' t (restrict (Base id) thin)
-    ~~ subst' t (Base $ id . thin)
-      ...(cong (subst' t) $ restrictBase id thin)
-    ~~ subst' t (Base thin)
-      ...(cong (subst' t . Base) $ identityLeft thin)
-    ~~ (t `Over` thin)
-      ...(substBase t thin)
+FullWeaken Ty CoTerm where
+  dropIsWkn (t `Over` thin) = ?dropIsWkn_rhs
+
+  wknCong = ?wknCong_rhs
+
+  wknId = ?wknId_rhs
+
+  wknHomo = ?wknHomo_rhs
+
+-- -- wknToTerm' :
+-- --   (t : FullTerm ty ctx) ->
+-- --   (thin : ctx `Thins` ctx') ->
+-- --   (thin' : ctx' `Thins` ctx''') ->
+-- --   wkn (toTerm' t thin) thin' = toTerm' t (thin' . thin)
+-- -- wknToTerm' Var thin thin' = cong Var (indexHomo thin' thin Here)
+-- -- wknToTerm' (Abs (MakeBound t (Drop Empty))) thin thin' =
+-- --   cong Abs (wknToTerm' t (Drop thin) (Keep thin'))
+-- -- wknToTerm' (Abs (MakeBound t (Keep Empty))) thin thin' =
+-- --   cong Abs (wknToTerm' t (Keep thin) (Keep thin'))
+-- -- wknToTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin thin' =
+-- --   rewrite sym $ assoc thin' thin thin1 in
+-- --   rewrite sym $ assoc thin' thin thin2 in
+-- --   cong2 App (wknToTerm' t (thin . thin1) thin') (wknToTerm' u (thin . thin2) thin')
+-- -- wknToTerm' Zero thin thin' = Refl
+-- -- wknToTerm' (Suc t) thin thin' = cong Suc (wknToTerm' t thin thin')
+-- -- wknToTerm'
+-- --   (Rec
+-- --     (MakePair
+-- --       (t `Over` thin1)
+-- --       (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin'') _))
+-- --   thin
+-- --   thin' =
+-- --   rewrite sym $ assoc thin' thin thin1 in
+-- --   rewrite sym $ assoc (thin' . thin) thin'' thin2 in
+-- --   rewrite sym $ assoc thin'  thin (thin'' . thin2) in
+-- --   rewrite sym $ assoc thin thin'' thin2 in
+-- --   rewrite sym $ assoc (thin' . thin) thin'' thin3 in
+-- --   rewrite sym $ assoc thin'  thin (thin'' . thin3) in
+-- --   rewrite sym $ assoc thin thin'' thin3 in
+-- --   cong3 Rec
+-- --     (wknToTerm' t (thin . thin1) thin')
+-- --     (wknToTerm' u (thin . (thin'' . thin2)) thin')
+-- --     (wknToTerm' v (thin . (thin'' . thin3)) thin')
+
+-- -- export
+-- -- wknToTerm :
+-- --   (t : CoTerm ty ctx) ->
+-- --   (thin : ctx `Thins` ctx') ->
+-- --   wkn (toTerm t) thin = toTerm (wkn t thin)
+-- -- wknToTerm (t `Over` thin') thin = wknToTerm' t thin' thin
+
+-- -- export
+-- -- toTermVar : Len ctx => (i : Elem ty ctx) -> toTerm (var i) = Var i
+-- -- toTermVar i = cong Var $ indexPoint i
+
+-- -- export
+-- -- toTermApp :
+-- --   (t : CoTerm (ty ~> ty') ctx) ->
+-- --   (u : CoTerm ty ctx) ->
+-- --   toTerm (app t u) = App (toTerm t) (toTerm u)
+-- -- toTermApp (t `Over` thin1) (u `Over` thin2) =
+-- --   cong2 App
+-- --     (cong (toTerm' t) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).left)
+-- --     (cong (toTerm' u) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).right)
+
+-- -- indexShift :
+-- --   (sub : Subst CoTerm ctx ctx') ->
+-- --   (i : Elem ty ctx) ->
+-- --   index (shift sub) i = drop (index sub i)
+-- -- indexShift (sub :< t) Here = Refl
+-- -- indexShift (sub :< t) (There i) = indexShift sub i
+
+-- -- indexBase : (thin : [<ty] `Thins` ctx') -> index (Base thin) Here = Var `Over` thin
+-- -- indexBase (Drop thin) = trans (indexShift (Base thin) Here) (cong drop (indexBase thin))
+-- -- indexBase (Keep thin) = irrelevantEq $ cong ((Var `Over`) . Keep) $ emptyUnique empty thin
+
+-- -- restrictShift :
+-- --   (sub : Subst CoTerm ctx' ctx'') ->
+-- --   (thin : ctx `Thins` ctx') ->
+-- --   restrict (shift sub) thin = shift (restrict sub thin)
+-- -- restrictShift [<] Empty = Refl
+-- -- restrictShift (sub :< t) (Drop thin) = restrictShift sub thin
+-- -- restrictShift (sub :< t) (Keep thin) = cong (:< drop t) (restrictShift sub thin)
+
+-- -- restrictBase :
+-- --   (thin2 : ctx' `Thins` ctx'') ->
+-- --   (thin1 : ctx `Thins` ctx') ->
+-- --   CoDebruijn.restrict (Base thin2) thin1 = Base (thin2 . thin1)
+-- -- restrictBase Empty Empty = Refl
+-- -- restrictBase (Drop thin2) thin1 =
+-- --   trans
+-- --     (restrictShift (Base thin2) thin1)
+-- --     (cong shift $ restrictBase thin2 thin1)
+-- -- restrictBase (Keep thin2) (Drop thin1) =
+-- --   trans
+-- --     (restrictShift (Base thin2) thin1)
+-- --     (cong shift $ restrictBase thin2 thin1)
+-- -- restrictBase (Keep thin2) (Keep thin1) =
+-- --   cong (:< (Var `Over` point Here)) $
+-- --   trans
+-- --     (restrictShift (Base thin2) thin1)
+-- --     (cong shift $ restrictBase thin2 thin1)
+
+-- substBase :
+--   (t : FullTerm ty ctx) ->
+--   (thin : ctx `Thins` ctx') ->
+--   subst' t (Base thin) = t `Over` thin
+-- -- substBase Var thin = indexBase thin
+-- -- substBase (Abs (MakeBound t (Drop Empty))) thin =
+-- --   Calc $
+-- --     |~ map Abs (MkBound (S Z) (subst' t (shift $ Base thin)))
+-- --     ~~ map Abs (MkBound (S Z) (t `Over` Drop thin))
+-- --       ...(cong (map Abs . MkBound (S Z)) $ substBase t (Drop thin))
+-- --     ~~ map Abs (MakeBound t (Drop Empty) `Over` thin)
+-- --       ...(Refl)
+-- --     ~~ (Abs (MakeBound t (Drop Empty)) `Over` thin)
+-- --       ...(Refl)
+-- -- substBase (Abs (MakeBound t (Keep Empty))) thin =
+-- --   Calc $
+-- --     |~ map Abs (MkBound (S Z) (subst' t (lift $ Base thin)))
+-- --     ~~ map Abs (MkBound (S Z) (t `Over` Keep thin))
+-- --       ...(cong (map Abs . MkBound (S Z)) $ substBase t (Keep thin))
+-- --     ~~ map Abs (MakeBound t (Keep Empty) `Over` thin)
+-- --       ...(Refl)
+-- --     ~~ (Abs (MakeBound t (Keep Empty)) `Over` thin)
+-- --       ...(Refl)
+-- -- substBase (App (MakePair (t `Over` thin1) (u `Over` thin2) cover)) thin =
+-- --   rewrite restrictBase thin thin1 in
+-- --   rewrite restrictBase thin thin2 in
+-- --   rewrite substBase t (thin . thin1) in
+-- --   rewrite substBase u (thin . thin2) in
+-- --   rewrite coprodEta thin cover in
+-- --   Refl
+-- -- substBase Zero thin = cong (Zero `Over`) $ irrelevantEq $ emptyUnique empty thin
+-- -- substBase (Suc t) thin = cong (map Suc) $ substBase t thin
+-- -- substBase
+-- --   (Rec (MakePair
+-- --       (t `Over` thin1)
+-- --       (MakePair
+-- --         (u `Over` thin2)
+-- --         (v `Over` thin3)
+-- --         cover'
+-- --       `Over` thin')
+-- --       cover))
+-- --   thin =
+-- --   rewrite restrictBase thin thin1 in
+-- --   rewrite restrictBase thin thin' in
+-- --   rewrite restrictBase (thin . thin') thin2 in
+-- --   rewrite restrictBase (thin . thin') thin3 in
+-- --   rewrite substBase t (thin . thin1) in
+-- --   rewrite substBase u ((thin . thin') . thin2) in
+-- --   rewrite substBase v ((thin . thin') . thin3) in
+-- --   rewrite coprodEta (thin . thin') cover' in
+-- --   rewrite coprodEta thin cover in
+-- --   Refl
+
+-- export
+-- substId : (t : CoTerm ty ctx) -> subst t (Base Id) = t
+-- substId (t `Over` thin) =
+--   Calc $
+--     |~ subst' t (restrict (Base Id) thin)
+--     ~~ subst' t (Base (Id . thin))        ...(cong (subst' t) $ restrictBase Id thin)
+--     ~~ subst' t (Base thin)               ...(Refl)
+--     ~~ (t `Over` thin)                    ...(substBase t thin)