WIP : use smarter weakenings.better-thinning

8 files changed, 662 insertions, 715 deletions

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)