Use co-deBruijn syntax in logical relation proof.master

Many proofs are still missing. Because they are erased, the program
still runs fine without them.

5 files changed, 657 insertions, 220 deletions

diff --git a/src/Thinning.idr b/src/Thinning.idr
index 70165d0..d2d65df 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -1,5 +1,6 @@
 module Thinning
 
+import Data.Singleton
 import Data.SnocList.Elem
 
 %prefix_record_projections off
@@ -38,7 +39,7 @@ lenAppend k Z = k
 lenAppend k (S m) = S (lenAppend k m)
 
 %hint
-export
+public export
 lenPred : Len (sx :< x) -> Len sx
 lenPred (S k) = k
 
@@ -59,7 +60,7 @@ id : (len : Len sx) => sx `Thins` sx
 id {len = Z} = Empty
 id {len = S k} = Keep id
 
-export
+public export
 point : Len sx => Elem ty sx -> [<ty] `Thins` sx
 point Here = Keep empty
 point (There i) = Drop (point i)
@@ -104,6 +105,7 @@ namespace Covering
     KeepDrop : Covering ov thin1 thin2 -> Covering ov (Keep thin1) (Drop thin2)
     KeepKeep : Covering Covers thin1 thin2 -> Covering Covers (Keep thin1) (Keep thin2)
 
+public export
 record Coproduct {sx, sy, sz : SnocList a} (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where
   constructor MkCoprod
   {0 sw : SnocList a}
@@ -114,6 +116,7 @@ record Coproduct {sx, sy, sz : SnocList a} (thin1 : sx `Thins` sz) (thin2 : sy `
   0 right : Triangle thin thin2' thin2
   0 cover : Covering Covers thin1' thin2'
 
+export
 coprod : (thin1 : sx `Thins` sz) -> (thin2 : sy `Thins` sz) -> Coproduct thin1 thin2
 coprod Empty Empty = MkCoprod EmptyAny EmptyAny EmptyEmpty
 coprod (Drop thin1) (Drop thin2) =
@@ -127,12 +130,14 @@ coprod (Keep thin1) (Keep 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)
@@ -160,7 +165,7 @@ public export
 Pair : (T, U : SnocList a -> Type) -> SnocList a -> Type
 Pair = OverlapPair Covers
 
-export
+public export
 MkPair : Thinned t sx -> Thinned u sx -> Thinned (OverlapPair Covers t u) sx
 MkPair (t `Over` thin1) (u `Over` thin2) =
   let cp = coprod thin1 thin2 in
@@ -173,20 +178,24 @@ record Binds (local : SnocList a) (T : SnocList a -> Type) (sx : SnocList a) whe
   value : T (sx ++ used)
   thin : used `Thins` local
 
-export
+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
 
-export
+public export
 map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx
 map f (value `Over` thin) = f value `Over` thin
 
-export
-drop : Thinned t ctx -> Thinned t (ctx :< ty)
+public export
+drop : Thinned t sx -> Thinned t (sx :< x)
 drop (value `Over` thin) = value `Over` Drop thin
 
+public export
+wkn : Thinned t sx -> sx `Thins` sy -> Thinned t sy
+wkn (value `Over` thin) thin' = value `Over` thin' . thin
+
 -- Properties ------------------------------------------------------------------
 
 export
@@ -195,6 +204,11 @@ lenUnique Z Z = Refl
 lenUnique (S k) (S m) = cong S (lenUnique k m)
 
 export
+emptyUnique : (thin1, thin2 : [<] `Thins` sx) -> thin1 = thin2
+emptyUnique Empty Empty = Refl
+emptyUnique (Drop thin1) (Drop thin2) = cong Drop (emptyUnique thin1 thin2)
+
+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)
@@ -239,3 +253,64 @@ 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)
+
+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
+
+export
+wknId : (len : Len sx) => (v : Thinned t sx) -> wkn v (id @{len}) = v
+wknId (value `Over` thin) = cong (value `Over`) $ identityLeft thin
+
+export
+wknHomo :
+  (v : Thinned t sx) ->
+  (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
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr
index 90bec66..b088e6f 100644
--- a/src/Total/LogRel.idr
+++ b/src/Total/LogRel.idr
@@ -1,32 +1,34 @@
 module Total.LogRel
 
+import Data.Singleton
 import Syntax.PreorderReasoning
 import Total.Reduction
 import Total.Term
+import Total.Term.CoDebruijn
 
 %prefix_record_projections off
 
 public export
 LogRel :
   {ctx : SnocList Ty} ->
-  (P : {ctx, ty : _} -> Term ctx ty -> Type) ->
+  (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) ->
   {ty : Ty} ->
-  (t : Term ctx ty) ->
+  (t : FullTerm 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 : Term ctx' ty) ->
+   (u : FullTerm ty ctx') ->
    LogRel p u ->
-   LogRel p (App (wkn t thin) u))
+   LogRel p (app (wkn t thin) u))
 
 export
 escape :
-  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
   {ty : Ty} ->
-  {0 t : Term ctx ty} ->
+  {0 t : FullTerm ty ctx} ->
   LogRel P t ->
   P t
 escape {ty = N} pt = pt
@@ -34,22 +36,22 @@ escape {ty = ty ~> ty'} (pt, app) = pt
 
 public export
 record PreserveHelper
-  (P : {ctx, ty : _} -> Term ctx ty -> Type)
-  (R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type) where
+  (P : {ctx, ty : _} -> FullTerm ty ctx -> Type)
+  (R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type) where
   constructor MkPresHelper
-  app :
-    {0 ctx : SnocList Ty} ->
+  0 app :
+    {ctx : SnocList Ty} ->
     {ty, ty' : Ty} ->
-    {0 t, u : Term ctx (ty ~> ty')} ->
+    (t, u : FullTerm (ty ~> ty') ctx) ->
     {ctx' : SnocList Ty} ->
     (thin : ctx `Thins` ctx') ->
-    (v : Term ctx' ty) ->
+    (v : FullTerm ty ctx') ->
     R t u ->
-    R (App (wkn t thin) v) (App (wkn u thin) v)
+    R (app (wkn t thin) v) (app (wkn u thin) v)
   pres :
     {0 ctx : SnocList Ty} ->
     {ty : Ty} ->
-    {0 t, u : Term ctx ty} ->
+    {0 t, u : FullTerm ty ctx} ->
     P t ->
     (0 _ : R t u) ->
     P u
@@ -58,35 +60,39 @@ record PreserveHelper
 
 export
 backStepHelper :
-  {0 P : {ctx, ty : _} -> Term ctx ty -> Type} ->
-  (forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> (0 _ : u > t) -> P u) ->
-  PreserveHelper P (flip (>))
+  {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) ->
+  PreserveHelper P (flip (>) `on` CoDebruijn.toTerm)
 backStepHelper pres =
   MkPresHelper
-    (\thin, v, step => AppCong1 (wknStep step))
+    (\t, u, thin, v, step =>
+      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))
     pres
 
 export
 preserve :
-  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
-  {R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type} ->
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  {0 R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type} ->
   {ty : Ty} ->
-  {0 t, u : Term ctx ty} ->
+  {0 t, u : FullTerm ty ctx} ->
   PreserveHelper P R ->
   LogRel P t ->
   (0 _ : R t u) ->
   LogRel P u
 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))
+  (help.pres pt prf, \thin, v, rel => preserve help (app thin v rel) (help.app _ _ thin v prf))
 
-data AllLogRel : (P : {ctx, ty : _} -> Term ctx ty -> Type) -> Terms ctx' ctx -> Type where
-  Base :
-    {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
-    {0 thin : ctx `Thins` ctx'} ->
-    AllLogRel P (Base thin)
+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 [<]
   (:<) :
-    {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+    {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
     AllLogRel P sub ->
     LogRel P t ->
     AllLogRel P (sub :< t)
@@ -94,48 +100,57 @@ data AllLogRel : (P : {ctx, ty : _} -> Term ctx ty -> Type) -> Terms ctx' ctx ->
 %name AllLogRel allRels
 
 index :
-  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
-  ((i : Elem ty ctx') -> LogRel P (Var i)) ->
-  {sub : Terms ctx' ctx} ->
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  ((i : Elem ty ctx') -> LogRel P (var i)) ->
+  {sub : CoTerms 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''} ->
+  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 : _} -> Term ctx ty -> Type) ->
+  (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) ->
   {ctx : SnocList Ty} ->
   {ty : Ty} ->
-  (t : Term ctx ty) ->
+  (t : FullTerm ty ctx) ->
   Type
 Valid p t =
   {ctx' : SnocList Ty} ->
-  (sub : Terms ctx' ctx) ->
+  (sub : CoTerms ctx ctx') ->
   (allRel : AllLogRel p sub) ->
   LogRel p (subst t sub)
 
 public export
-record ValidHelper (P : {ctx, ty : _} -> Term ctx ty -> Type) where
+record ValidHelper (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) where
   constructor MkValidHelper
-  var : forall ctx. {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (Var i)
-  abs : forall ctx, ty. {ty' : Ty} -> {0 t : Term (ctx :< ty) ty'} -> LogRel P t -> P (Abs t)
-  zero : forall ctx. P {ctx} Zero
-  suc : forall ctx. {0 t : Term ctx N} -> P t -> P (Suc t)
+  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)
   rec :
     {ctx : SnocList Ty} ->
     {ty : Ty} ->
-    {0 t : Term ctx N} ->
-    {u : Term ctx ty} ->
-    {v : Term ctx (ty ~> ty)} ->
+    {0 t : FullTerm N ctx} ->
+    {u : FullTerm ty ctx} ->
+    {v : FullTerm (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 : Term ctx ty} -> P t -> (0 _ : u > t) -> P u
+    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
   wkn : forall ctx, ctx', ty.
-    {0 t : Term ctx ty} ->
+    {0 t : FullTerm ty ctx} ->
     P t ->
     (thin : ctx `Thins` ctx') ->
     P (wkn t thin)
@@ -143,100 +158,198 @@ record ValidHelper (P : {ctx, ty : _} -> Term ctx ty -> Type) where
 %name ValidHelper help
 
 wknRel :
-  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
   ValidHelper P ->
   {ty : Ty} ->
-  {0 t : Term ctx ty} ->
+  {0 t : FullTerm 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 =>
+    rewrite wknHomo t thin' thin in
+    app (thin' . thin) u rel
   )
 
 wknAllRel :
-  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
   ValidHelper P ->
   {ctx : SnocList Ty} ->
-  {sub : Terms ctx' ctx} ->
+  {sub : CoTerms ctx ctx'} ->
   AllLogRel P sub ->
   (thin : ctx' `Thins` ctx'') ->
   AllLogRel P (wknAll sub thin)
-wknAllRel help Base thin = Base
+wknAllRel help [<] thin = [<]
 wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin
 
-export
-allValid :
-  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
-  {ctx : SnocList Ty} ->
+shiftRel :
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  ValidHelper P ->
+  {ctx, ctx' : SnocList Ty} ->
+  {sub : CoTerms ctx ctx'} ->
+  AllLogRel P sub ->
+  AllLogRel P (shift {ty} sub)
+shiftRel help [<] = [<]
+shiftRel help (allRels :< rel) =
+  shiftRel help allRels :<
+  replace {p = LogRel P} (sym $ dropIsWkn _) (wknRel help rel (Drop id))
+
+liftRel :
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  ValidHelper P ->
+  {ctx, ctx' : SnocList Ty} ->
   {ty : Ty} ->
+  {sub : CoTerms ctx ctx'} ->
+  AllLogRel P sub ->
+  AllLogRel P (lift {ty} sub)
+liftRel help allRels = shiftRel help allRels :< help.var Here
+
+absValid :
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
   ValidHelper P ->
-  (t : Term ctx ty) ->
-  Valid P t
-allValid help (Var i) sub allRels = index help.var allRels i
-allValid help (Abs t) sub allRels =
-  let valid = allValid help t in
-  (let
-      rec =
-        valid
-          (wknAll sub (Drop id) :< Var Here)
-          (wknAllRel help allRels (Drop id) :< help.var Here)
-    in
-      help.abs rec
+  {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 =>
-    let
-      eq :
-        (subst
-          (wkn (subst t (wknAll 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 t (Base (thin . id) . sub :< u)
-            ...(cong (subst t . (:< u)) $ compWknAll sub (Base thin :< u) (Drop id))
-          ~~ subst t (Base thin . sub :< u)
-            ...(cong (subst t . (:< u) . (. sub) . Base) $ identityRight thin)
-          ~~ subst t (wknAll sub thin :< u)
-            ...(cong (subst t . (:< u)) $ baseComp thin sub)
-    in
-      preserve
-        (backStepHelper help.step)
-        (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel))
-        (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)}
-          eq
-          (AppBeta (length _)))
+    preserve
+      (backStepHelper help.step)
+      (valid (wknAll sub thin) (wknAllRel help allRels thin))
+      ?betaStep
   )
-allValid help (App t u) sub allRels =
+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'
+  )
+
+export
+allValid :
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  ValidHelper P ->
+  (s : Singleton ctx) =>
+  {ty : Ty} ->
+  (t : FullTerm ty ctx) ->
+  Valid P t
+allValid' :
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
+  ValidHelper P ->
+  (s : Singleton ctx) =>
+  {ty : Ty} ->
+  (t : CoTerm ty ctx) ->
+  {ctx' : SnocList Ty} ->
+  (sub : CoTerms ctx ctx') ->
+  AllLogRel P sub ->
+  LogRel P (subst' t sub)
+
+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 (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
-allValid help Zero sub allRels = help.zero
-allValid help (Suc t) sub allRels =
-  let pt = allValid help t sub allRels 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
   help.suc pt
-allValid help (Rec t u v) sub allRels =
-  let relt = allValid help t sub allRels in
-  let relu = allValid help u sub allRels in
-  let relv = allValid help v sub allRels in
-  help.rec relt relu relv
+allValid' help (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub allRels =
+  let relT = allValid help t sub allRels in
+  let relU = allValid help u (restrict sub thin) (restrict allRels thin) in
+  let relV = allValid help v (restrict sub thin) (restrict allRels thin) in
+  help.rec relT relU relV
+
+-- -- allValid help (Var i) sub allRels = index help.var allRels i
+-- -- allValid help (Abs t) sub allRels =
+-- --   let valid = allValid help t in
+-- --   (let
+-- --       rec =
+-- --         valid
+-- --           (wknAll sub (Drop id) :< Var Here)
+-- --           (wknAllRel help allRels (Drop id) :< help.var Here)
+-- --     in
+-- --       help.abs rec
+-- --   , \thin, u, rel =>
+-- --     let
+-- --       eq :
+-- --         (subst
+-- --           (wkn (subst t (wknAll 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 t (Base (thin . id) . sub :< u)
+-- --             ...(cong (subst t . (:< u)) $ compWknAll sub (Base thin :< u) (Drop id))
+-- --           ~~ subst t (Base thin . sub :< u)
+-- --             ...(cong (subst t . (:< u) . (. sub) . Base) $ identityRight thin)
+-- --           ~~ subst t (wknAll sub thin :< u)
+-- --             ...(cong (subst t . (:< u)) $ baseComp thin sub)
+-- --     in
+-- --       preserve
+-- --         (backStepHelper help.step)
+-- --         (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel))
+-- --         (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)}
+-- --           eq
+-- --           (AppBeta (length _)))
+-- --   )
+-- -- allValid help (App t u) sub allRels =
+-- --   let (pt, app) = allValid help t sub allRels in
+-- --   let rel = allValid help u sub allRels in
+-- --   rewrite sym $ wknId (subst t sub) in
+-- --     app id (subst u sub) rel
+-- -- allValid help Zero sub allRels = help.zero
+-- -- allValid help (Suc t) sub allRels =
+-- --   let pt = allValid help t sub allRels in
+-- --   help.suc pt
+-- -- allValid help (Rec t u v) sub allRels =
+-- --   let relt = allValid help t sub allRels in
+-- --   let relu = allValid help u sub allRels in
+-- --   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)
 
 export
 allRel :
-  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
   {ctx : SnocList Ty} ->
   {ty : Ty} ->
   ValidHelper P ->
-  (t : Term ctx ty) ->
+  (t : FullTerm ty ctx) ->
   P t
 allRel help t =
-  rewrite sym $ substId t in escape (allValid help t (Base id) Base)
+  rewrite sym $ substId t in
+  escape {P} $
+  allValid help @{Val ctx} t (Base id) (idRel help)
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
index 266d00d..a7aba57 100644
--- a/src/Total/NormalForm.idr
+++ b/src/Total/NormalForm.idr
@@ -3,143 +3,185 @@ module Total.NormalForm
 import Total.LogRel
 import Total.Reduction
 import Total.Term
+import Total.Term.CoDebruijn
 
 %prefix_record_projections off
 
 public export
-data Neutral : Term ctx ty -> Type
+data Neutral' : CoTerm ty ctx -> Type
 public export
-data Normal : Term ctx ty -> Type
+data Normal' : CoTerm ty ctx -> Type
+
+public export
+data Neutral : FullTerm ty ctx -> Type
+
+public export
+data Normal : FullTerm ty ctx -> Type
+
+data Neutral' where
+  Var : Neutral' Var
+  App : Neutral t -> Normal u -> Neutral' (App (MakePair t u cover))
+  Rec :
+    Neutral t ->
+    Normal u ->
+    Normal v ->
+    Neutral' (Rec (MakePair t (MakePair u v cover1 `Over` thin) cover2))
+
+data Normal' where
+  Ntrl : Neutral' t -> Normal' t
+  Abs : Normal' t -> Normal' (Abs (MakeBound t thin))
+  Zero : Normal' Zero
+  Suc : Normal' t -> Normal' (Suc t)
 
 data Neutral where
-  Var : Neutral (Var i)
-  App : Neutral t -> Normal u -> Neutral (App t u)
-  Rec : Neutral t -> Normal u -> Normal v -> Neutral (Rec t u v)
+  WrapNe : Neutral' t -> Neutral (t `Over` thin)
 
 data Normal where
-  Ntrl : Neutral t -> Normal t
-  Abs : Normal t -> Normal (Abs t)
-  Zero : Normal Zero
-  Suc : Normal t -> Normal (Suc t)
+  WrapNf : Normal' t -> Normal (t `Over` thin)
 
 %name Neutral n, m, k
 %name Normal n, m, k
+%name Neutral' n, m, k
+%name Normal' n, m, k
 
 public export
-record NormalForm (0 t : Term ctx ty) where
+record NormalForm (0 t : FullTerm ty ctx) where
   constructor MkNf
-  term : Term ctx ty
-  0 steps : t >= term
+  term : FullTerm ty ctx
+  0 steps : toTerm t >= toTerm term
   0 normal : Normal term
 
 %name NormalForm nf
 
 -- Strong Normalization Proof --------------------------------------------------
 
-invApp : Normal (App t u) -> Neutral (App t u)
+abs : Normal t -> Normal (abs t)
+
+app : Neutral t -> Normal u -> Neutral (app t u)
+
+suc : Normal t -> Normal (suc t)
+
+rec : Neutral t -> Normal u -> Normal v -> Neutral (rec t u v)
+
+invApp : Normal' (App x) -> Neutral' (App x)
 invApp (Ntrl n) = n
 
-invRec : Normal (Rec t u v) -> Neutral (Rec t u v)
+invRec : Normal' (Rec x) -> Neutral' (Rec x)
 invRec (Ntrl n) = n
 
-invSuc : Normal (Suc t) -> Normal t
+invSuc : Normal' (Suc t) -> Normal' t
 invSuc (Suc n) = n
 
 wknNe : Neutral t -> Neutral (wkn t thin)
-wknNf : Normal t -> Normal (wkn t thin)
-
-wknNe Var = Var
-wknNe (App n m) = App (wknNe n) (wknNf m)
-wknNe (Rec n m k) = Rec (wknNe n) (wknNf m) (wknNf k)
+wknNe (WrapNe n) = WrapNe n
 
-wknNf (Ntrl n) = Ntrl (wknNe n)
-wknNf (Abs n) = Abs (wknNf n)
-wknNf Zero = Zero
-wknNf (Suc n) = Suc (wknNf n)
+wknNf : Normal t -> Normal (wkn t thin)
+wknNf (WrapNf n) = WrapNf n
 
-backStepsNf : NormalForm t -> (0 _ : u >= t) -> NormalForm u
+backStepsNf : NormalForm t -> (0 _ : toTerm u >= toTerm t) -> NormalForm u
 backStepsNf nf steps = MkNf nf.term (steps ++ nf.steps) nf.normal
 
 backStepsRel :
   {ty : Ty} ->
-  {0 t, u : Term ctx ty} ->
+  {0 t, u : FullTerm ty ctx} ->
   LogRel (\t => NormalForm t) t ->
-  (0 _ : u >= t) ->
+  (0 _ : toTerm u >= toTerm t) ->
   LogRel (\t => NormalForm t) u
 backStepsRel =
-  preserve {R = flip (>=)}
-    (MkPresHelper (\thin, v, steps => AppCong1' (wknSteps steps)) backStepsNf)
-
-ntrlRel : {ty : Ty} -> {t : Term ctx ty} -> (0 _ : Neutral t) -> LogRel (\t => NormalForm t) t
-ntrlRel {ty = N} n = MkNf t [<] (Ntrl n)
-ntrlRel {ty = ty ~> ty'} n =
-  ( MkNf t [<] (Ntrl n)
+  preserve {R = flip (>=) `on` toTerm}
+    (MkPresHelper
+      (\t, u, thin, v, steps =>
+        ?appCong1Steps)
+      backStepsNf)
+
+ntrlRel : {ty : Ty} -> {t : FullTerm ty ctx} -> (0 _ : Neutral t) -> LogRel (\t => NormalForm t) t
+ntrlRel {ty = N} (WrapNe n) = MkNf t [<] (WrapNf (Ntrl n))
+ntrlRel {ty = ty ~> ty'} (WrapNe {thin = thin'} n) =
+  ( MkNf t [<] (WrapNf (Ntrl n))
   , \thin, u, rel =>
     backStepsRel
-      (ntrlRel (App (wknNe n) (escape rel).normal))
-      (AppCong2' (escape rel).steps)
+      (ntrlRel (app (wknNe {thin} (WrapNe {thin = thin'} n)) (escape rel).normal))
+      ?appCong2Steps
   )
 
-recNf' :
+recNf'' :
   {ctx : SnocList Ty} ->
   {ty : Ty} ->
-  {u : Term ctx ty} ->
-  {v : Term ctx (ty ~> ty)} ->
-  (t' : Term ctx N) ->
-  (0 n : Normal t') ->
+  {u : FullTerm ty ctx} ->
+  {v : FullTerm (ty ~> ty) ctx} ->
+  (t : CoTerm N ctx') ->
+  (thin : ctx' `Thins` ctx) ->
+  (0 n : Normal' t) ->
   LogRel (\t => NormalForm t) u ->
   LogRel (\t => NormalForm t) v ->
-  LogRel (\t => NormalForm t) (Rec t' u v)
-recNf' Zero n relU relV = backStepsRel relU [<RecZero]
-recNf' (Suc t') n relU relV =
-  let rec = recNf' t' (invSuc n) relU relV in
-  let step : Rec (Suc t') u v > App (wkn v id) (Rec t' u v) = rewrite wknId v in RecSuc in
-  backStepsRel (snd relV id _ rec) [<step]
-recNf' t'@(Var _) n relU relV =
+  LogRel (\t => NormalForm t) (rec (t `Over` thin) u v)
+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]
+recNf'' t@Var thin n relU relV =
+  let 0 neT = WrapNe {thin} Var in
   let nfU = escape relU in
   let nfV = escape {ty = ty ~> ty} relV in
   backStepsRel
-    (ntrlRel (Rec Var nfU.normal nfV.normal))
-    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
-recNf' t'@(App _ _) n relU relV =
+    (ntrlRel (rec neT nfU.normal nfV.normal))
+    ?stepsUandV
+recNf'' t@(App _) thin n relU relV =
+  let 0 neT = WrapNe {thin} (invApp n) in
   let nfU = escape relU in
   let nfV = escape {ty = ty ~> ty} relV in
   backStepsRel
-    (ntrlRel (Rec (invApp n) nfU.normal nfV.normal))
-    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
-recNf' t'@(Rec _ _ _) n relU relV =
+    (ntrlRel (rec neT nfU.normal nfV.normal))
+    ?stepsUandV'
+recNf'' t@(Rec _) thin n relU relV =
+  let 0 neT = WrapNe {thin} (invRec n) in
   let nfU = escape relU in
   let nfV = escape {ty = ty ~> ty} relV in
   backStepsRel
-    (ntrlRel (Rec (invRec n) nfU.normal nfV.normal))
-    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
+    (ntrlRel (rec neT nfU.normal nfV.normal))
+    ?stepsUandV''
+
+recNf' :
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  {u : FullTerm ty ctx} ->
+  {v : FullTerm (ty ~> ty) ctx} ->
+  (t : FullTerm N ctx) ->
+  (0 n : Normal t) ->
+  LogRel (\t => NormalForm t) u ->
+  LogRel (\t => NormalForm t) v ->
+  LogRel (\t => NormalForm t) (rec t u v)
+recNf' (t `Over` thin) (WrapNf n) = recNf'' t thin n
 
 recNf :
   {ctx : SnocList Ty} ->
   {ty : Ty} ->
-  {0 t : Term ctx N} ->
-  {u : Term ctx ty} ->
-  {v : Term ctx (ty ~> ty)} ->
+  {0 t : FullTerm N ctx} ->
+  {u : FullTerm ty ctx} ->
+  {v : FullTerm (ty ~> ty) ctx} ->
   NormalForm t ->
   LogRel (\t => NormalForm t) u ->
   LogRel (\t => NormalForm t) v ->
-  LogRel (\t => NormalForm t) (Rec t u v)
+  LogRel (\t => NormalForm t) (rec t u v)
 recNf nf relU relV =
   backStepsRel
     (recNf' nf.term nf.normal relU relV)
-    (RecCong1' nf.steps)
+    ?recCong1Steps
 
 helper : ValidHelper (\t => NormalForm t)
 helper = MkValidHelper
-  { var = \i => ntrlRel Var
-  , abs = \rel => let nf = escape rel in MkNf (Abs nf.term) (AbsCong' nf.steps) (Abs nf.normal)
-  , zero = MkNf Zero [<] Zero
-  , suc = \nf => MkNf (Suc nf.term) (SucCong' nf.steps) (Suc nf.normal)
+  { var = \i => ntrlRel (WrapNe Var)
+  , abs = \rel =>
+    let nf = escape rel in
+    MkNf (abs nf.term) ?absCongSteps (abs nf.normal)
+  , zero = MkNf zero [<] (WrapNf Zero)
+  , suc = \nf => MkNf (suc nf.term) ?sucCongSteps (suc nf.normal)
   , rec = recNf
   , step = \nf, step => backStepsNf nf [<step]
-  , wkn = \nf, thin => MkNf (wkn nf.term thin) (wknSteps nf.steps) (wknNf nf.normal)
+  , wkn = \nf, thin => MkNf (wkn nf.term thin) ?wknSteps (wknNf nf.normal)
   }
 
 export
-normalize : {ctx : SnocList Ty} -> {ty : Ty} -> (t : Term ctx ty) -> NormalForm t
+normalize : {ctx : SnocList Ty} -> {ty : Ty} -> (t : FullTerm ty ctx) -> NormalForm t
 normalize = allRel helper
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 8e3e42a..129662a 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -77,6 +77,7 @@ sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2
 
 -- Utilities
 
+export
 cong3 : (0 f : a -> b -> c -> d) -> x1 = x2 -> y1 = y2 -> z1 = z2 -> f x1 y1 z1 = f x2 y2 z2
 cong3 f Refl Refl Refl = Refl
 
diff --git a/src/Total/Term/CoDebruijn.idr b/src/Total/Term/CoDebruijn.idr
index 00abc31..0efcdbb 100644
--- a/src/Total/Term/CoDebruijn.idr
+++ b/src/Total/Term/CoDebruijn.idr
@@ -7,6 +7,8 @@ import Total.Term
 
 %prefix_record_projections off
 
+-- Definition ------------------------------------------------------------------
+
 public export
 data CoTerm : Ty -> SnocList Ty -> Type where
   Var : CoTerm ty [<ty]
@@ -22,90 +24,294 @@ public export
 FullTerm : Ty -> SnocList Ty -> Type
 FullTerm ty ctx = Thinned (CoTerm ty) ctx
 
-export
+-- Smart Constructors ----------------------------------------------------------
+
+public export
 var : Len ctx => Elem ty ctx -> FullTerm ty ctx
 var i = Var `Over` point i
 
-export
+public export
 abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx
 abs = map Abs . MkBound (S Z)
 
-export
+public export
 app : {ty : Ty} -> FullTerm (ty ~> ty') ctx -> FullTerm ty ctx -> FullTerm ty' ctx
 app t u = map App (MkPair t u)
 
-export
+public export
 zero : Len ctx => FullTerm N ctx
 zero = Zero `Over` empty
 
-export
+public export
 suc : FullTerm N ctx -> FullTerm N ctx
 suc = map Suc
 
-export
+public export
 rec : FullTerm N ctx -> FullTerm ty ctx -> FullTerm (ty ~> ty) ctx -> FullTerm ty ctx
 rec t u v = map Rec $ MkPair t (MkPair u v)
 
-export
-wkn : FullTerm ty ctx -> ctx `Thins` ctx' -> FullTerm ty ctx'
-wkn (t `Over` thin) thin' = t `Over` thin' . thin
+-- Substitutions ---------------------------------------------------------------
 
 public export
 data CoTerms : SnocList Ty -> SnocList Ty -> Type where
-  Base : ctx `Thins` ctx' -> CoTerms ctx ctx'
+  Lin : CoTerms [<] ctx'
   (:<) : CoTerms ctx ctx' -> FullTerm ty ctx' -> CoTerms (ctx :< ty) ctx'
 
 %name CoTerms sub
 
-export
+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 (Base thin) = Base (Drop thin)
-shift (sub :< (t `Over` thin)) = shift sub :< (t `Over` Drop thin)
+shift [<] = [<]
+shift (sub :< t) = shift sub :< drop t
 
-export
+public export
 lift : Len ctx' => CoTerms ctx ctx' -> CoTerms (ctx :< ty) (ctx' :< ty)
 lift sub = shift sub :< var Here
 
-export
+public export
 restrict : CoTerms ctx' ctx'' -> ctx `Thins` ctx' -> CoTerms ctx ctx''
-restrict (Base thin') thin = Base (thin' . thin)
+restrict [<] Empty = [<]
 restrict (sub :< t) (Drop thin) = restrict sub thin
 restrict (sub :< t) (Keep thin) = restrict sub thin :< t
 
-export
+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)
+
+-- Substitution Operation ------------------------------------------------------
+
+public export
 subst : Len ctx' => FullTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
+public export
 subst' : Len ctx' => CoTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
 
 subst (t `Over` thin) sub = subst' t (restrict sub thin)
 
-subst' t (Base thin) = t `Over` thin
-subst' Var (sub :< t) = t
-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' (App (MakePair t u _)) sub@(_ :< _) = app (subst t sub) (subst u sub)
-subst' (Suc t) sub@(_ :< _) = suc (subst' t sub)
-subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub@(_ :< _) =
+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' (App (MakePair t u _)) sub = app (subst t sub) (subst u sub)
+subst' Zero sub = zero
+subst' (Suc t) sub = suc (subst' t sub)
+subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub =
   rec (subst t sub) (subst u (restrict sub thin)) (subst v (restrict sub thin))
 
-toTerm : CoTerm ty ctx -> ctx `Thins` ctx' -> Term ctx' ty
-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 (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
-  App (toTerm t (thin . thin1)) (toTerm u (thin . thin2))
-toTerm Zero thin = Zero
-toTerm (Suc t) thin = Suc (toTerm t thin)
-toTerm
+-- Initiality ------------------------------------------------------------------
+
+toTerm' : CoTerm ty ctx -> ctx `Thins` ctx' -> Term ctx' ty
+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' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
+  App (toTerm' t (thin . thin1)) (toTerm' u (thin . thin2))
+toTerm' Zero thin = Zero
+toTerm' (Suc t) thin = Suc (toTerm' t thin)
+toTerm'
   (Rec
     (MakePair
       (t `Over` thin1)
       (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin') _))
   thin =
   Rec
-    (toTerm t (thin . thin1))
-    (toTerm u ((thin . thin') . thin2))
-    (toTerm v ((thin . thin') . thin3))
+    (toTerm' t (thin . thin1))
+    (toTerm' u ((thin . thin') . thin2))
+    (toTerm' v ((thin . thin') . thin3))
+
+export
+toTerm : FullTerm ty ctx -> Term ctx ty
+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 (t `Over` thin) = toTerm t thin
+  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)
+
+-- 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
+
+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)