Reset using only co-de Bruijn syntax.

8 files changed, 0 insertions, 2065 deletions

diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr
deleted file mode 100644
index f56d1bc..0000000
--- a/src/Total/Encoded/Util.idr
+++ /dev/null
@@ -1,444 +0,0 @@
-module Total.Encoded.Util
-
-import public Data.Fin
-import public Data.List1
-import public Data.List.Elem
-import public Data.List.Quantifiers
-import public Total.Syntax
-
-%prefix_record_projections off
-
-namespace Bool
-  export
-  B : Ty
-  B = N
-
-  export
-  true : FullTerm B [<]
-  true = zero
-
-  export
-  false : FullTerm B [<]
-  false = suc zero
-
-  export
-  if' : FullTerm (B ~> ty ~> ty ~> ty) [<]
-  if' = abs' (S $ S $ S Z) (\b, t, f => rec b t (abs $ drop f))
-
-namespace Arb
-  export
-  arb : {ty : Ty} -> FullTerm ty [<]
-  arb {ty = N} = zero
-  arb {ty = ty ~> ty'} = abs (lift arb)
-
-namespace Union
-  export
-  (<+>) : Ty -> Ty -> Ty
-  N <+> N = N
-  N <+> (u ~> u') = u ~> u'
-  (t ~> t') <+> N = t ~> t'
-  (t ~> t') <+> (u ~> u') = (t <+> u) ~> (t' <+> u')
-
-  export
-  swap : {t, u : Ty} -> FullTerm ((t <+> u) ~> (u <+> t)) [<]
-  swap {t = N, u = N} = id
-  swap {t = N, u = u ~> u'} = id
-  swap {t = t ~> t', u = N} = id
-  swap {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop swap . f . drop swap)
-
-  export
-  injL : {t, u : Ty} -> FullTerm (t ~> (t <+> u)) [<]
-  export
-  injR : {t, u : Ty} -> FullTerm (u ~> (t <+> u)) [<]
-  export
-  prjL : {t, u : Ty} -> FullTerm ((t <+> u) ~> t) [<]
-  export
-  prjR : {t, u : Ty} -> FullTerm ((t <+> u) ~> u) [<]
-
-  injL {t = N, u = N} = id
-  injL {t = N, u = u ~> u'} = abs' (S $ S Z) (\n, _ => app (lift (prjR . injL)) n)
-  injL {t = t ~> t', u = N} = id
-  injL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop injL . f . drop prjL)
-
-  injR = swap . injL
-
-  prjL {t = N, u = N} = id
-  prjL {t = N, u = u ~> u'} = abs' (S Z) (\f => app (drop (prjL . injR) . f) (drop arb))
-  prjL {t = t ~> t', u = N} = id
-  prjL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop prjL . f . drop injL)
-
-  prjR = prjL . swap
-
-namespace Unit
-  export
-  Unit : Ty
-  Unit = N
-
-namespace Pair
-  export
-  (*) : Ty -> Ty -> Ty
-  t * u = B ~> (t <+> u)
-
-  export
-  pair : {t, u : Ty} -> FullTerm (t ~> u ~> (t * u)) [<]
-  pair = abs' (S $ S $ S Z)
-    (\fst, snd, b => app' (lift if') [<b, app (lift injL) fst, app (lift injR) snd])
-
-  export
-  fst : {t, u : Ty} -> FullTerm ((t * u) ~> t) [<]
-  fst = abs' (S Z) (\p => app (drop prjL . p) (drop true))
-
-  export
-  snd : {t, u : Ty} -> FullTerm ((t * u) ~> u) [<]
-  snd = abs' (S Z) (\p => app (drop prjR . p) (drop false))
-
-  export
-  mapSnd : {t, u, v : Ty} -> FullTerm ((u ~> v) ~> (t * u) ~> (t * v)) [<]
-  mapSnd = abs' (S $ S Z) (\f, p => app' (lift pair) [<app (lift fst) p , app (f . lift snd) p])
-
-  export
-  Product : SnocList Ty -> Ty
-  Product = foldl (*) Unit
-
-  export
-  pair' : {tys : SnocList Ty} -> FullTerm (tys ~>* Product tys) [<]
-  pair' {tys = [<]} = arb
-  pair' {tys = tys :< ty} = abs' (S $ S Z) (\p, t => app' (lift pair) [<p, t]) .* pair'
-
-  export
-  project : {tys : SnocList Ty} -> Elem ty tys -> FullTerm (Product tys ~> ty) [<]
-  project {tys = tys :< ty} Here = snd
-  project {tys = tys :< ty} (There i) = project i . fst
-
-  export
-  mapProd :
-    {ctx, tys, tys' : SnocList Ty} ->
-    {auto 0 prf : SnocList.length tys = SnocList.length tys'} ->
-    All (flip FullTerm ctx) (zipWith (~>) tys tys') ->
-    FullTerm (Product tys ~> Product tys') ctx
-  mapProd {tys = [<], tys' = [<]} [<] = lift id
-  mapProd {tys = tys :< ty, tys' = tys' :< ty', prf} (fs :< f) =
-    abs' (S Z)
-      (\p =>
-        app' (lift pair)
-          [<app (drop (mapProd fs {prf = injective prf}) . lift fst) p
-          , app (drop f . lift snd) p
-          ])
-
-  replicate : Nat -> a -> SnocList a
-  replicate 0 x = [<]
-  replicate (S n) x = replicate n x :< x
-
-  replicateLen : (n : Nat) -> SnocList.length (replicate n x) = n
-  replicateLen 0 = Refl
-  replicateLen (S k) = cong S (replicateLen k)
-
-  export
-  Vect : Nat -> Ty -> Ty
-  Vect n ty = Product (replicate n ty)
-
-  zipReplicate :
-    {0 f : a -> b -> c} ->
-    {0 p : c -> Type} ->
-    {n : Nat} ->
-    p (f x y) ->
-    SnocList.Quantifiers.All.All p (zipWith f (replicate n x) (replicate n y))
-  zipReplicate {n = 0} z = [<]
-  zipReplicate {n = S k} z = zipReplicate z :< z
-
-  export
-  mapVect :
-    {n : Nat} ->
-    {ty, ty' : Ty} ->
-    FullTerm ((ty ~> ty') ~> Vect n ty ~> Vect n ty') [<]
-  mapVect =
-    abs' (S Z)
-      (\f => mapProd {prf = trans (replicateLen n) (sym $ replicateLen n)} $ zipReplicate f)
-
-  export
-  nil : {ty : Ty} -> FullTerm (Vect 0 ty) [<]
-  nil = arb
-
-  export
-  cons : {n : Nat} -> {ty : Ty} -> FullTerm (ty ~> Vect n ty ~> Vect (S n) ty) [<]
-  cons = abs' (S $ S Z) (\t, ts => app' (lift pair) [<ts, t])
-
-  export
-  head : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> ty) [<]
-  head = snd
-
-  export
-  tail : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> Vect n ty) [<]
-  tail = fst
-
-  export
-  index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> FullTerm (Vect n ty ~> ty) [<]
-  index FZ = head
-  index (FS i) = index i . tail
-
-  export
-  enumerate : (n : Nat) -> FullTerm (Vect n N) [<]
-  enumerate 0 = arb
-  enumerate (S k) = app' pair [<app' mapVect [<abs' (S Z) suc, enumerate k], zero]
-
-namespace Sum
-  export
-  (+) : Ty -> Ty -> Ty
-  t + u = B * (t <+> u)
-
-  export
-  left : {t, u : Ty} -> FullTerm (t ~> (t + u)) [<]
-  left = abs' (S Z) (\e => app' (drop pair) [<drop true, app (drop injL) e])
-
-  export
-  right : {t, u : Ty} -> FullTerm (u ~> (t + u)) [<]
-  right = abs' (S Z) (\e => app' (drop pair) [<drop false, app (drop injR) e])
-
-  export
-  case' : {t, u, ty : Ty} -> FullTerm ((t + u) ~> (t ~> ty) ~> (u ~> ty) ~> ty) [<]
-  case' = abs' (S $ S $ S Z)
-    (\s, f, g =>
-      app' (lift if')
-        [<app (lift fst) s
-        , app (f . lift (prjL . snd)) s
-        , app (g . lift (prjR . snd)) s])
-
-  export
-  either : {t, u, ty : Ty} -> FullTerm ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty) [<]
-  either = abs' (S $ S $ S Z) (\f, g, s => app' (lift case') [<s, f, g])
-
-  Sum' : Ty -> List Ty -> Ty
-  Sum' ty [] = ty
-  Sum' ty (ty' :: tys) = ty + Sum' ty' tys
-
-  export
-  Sum : List1 Ty -> Ty
-  Sum (ty ::: tys) = Sum' ty tys
-
-  put' :
-    {ty, ty' : Ty} ->
-    {tys : List Ty} ->
-    (i : Elem ty (ty' :: tys)) ->
-    FullTerm (ty ~> Sum' ty' tys) [<]
-  put' {tys = []} Here = id
-  put' {tys = _ :: _} Here = left
-  put' {tys = _ :: _} (There i) = right . put' i
-
-  export
-  put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> FullTerm (ty ~> Sum tys) [<]
-  put {tys = _ ::: _} i = put' i
-
-  any' :
-    {ctx : SnocList Ty} ->
-    {ty, ty' : Ty} ->
-    {tys : List Ty} ->
-    All (flip FullTerm ctx . (~> ty)) (ty' :: tys) ->
-    FullTerm (Sum' ty' tys ~> ty) ctx
-  any' (t :: []) = t
-  any' (t :: u :: ts) = app' (lift either) [<t, any' (u :: ts)]
-
-  export
-  any :
-    {ctx : SnocList Ty} ->
-    {tys : List1 Ty} ->
-    {ty : Ty} ->
-    All (flip FullTerm ctx . (~> ty)) (forget tys) ->
-    FullTerm (Sum tys ~> ty) ctx
-  any {tys = _ ::: _} = any'
-
-namespace Nat
-  export
-  isZero : FullTerm (N ~> B) [<]
-  isZero = abs' (S Z) (\m => rec m (drop true) (abs (lift false)))
-
-  export
-  add : FullTerm (N ~> N ~> N) [<]
-  add = abs' (S $ S Z) (\m, n => rec m n (abs' (S Z) suc))
-
-  export
-  sum : {n : Nat} -> FullTerm (Vect n N ~> N) [<]
-  sum {n = 0} = abs zero
-  sum {n = S k} = abs' (S Z)
-    (\ns => app' (lift add) [<app (lift head) ns, app (lift (sum . tail)) ns])
-
-  export
-  pred : FullTerm (N ~> N) [<]
-  pred = abs' (S Z)
-    (\m =>
-      app' (lift case')
-        [<rec m
-            (lift $ app left (arb {ty = Unit}))
-            (app' (lift either)
-              [<abs (lift $ app right zero)
-              , abs' (S Z) (\n => app (lift right) (suc n))
-              ])
-        , abs zero
-        , drop id
-        ])
-
-  export
-  sub : FullTerm (N ~> N ~> N) [<]
-  sub = abs' (S $ S Z) (\m, n => rec n m (lift pred))
-
-  export
-  le : FullTerm (N ~> N ~> B) [<]
-  le = abs' (S Z) (\m => lift isZero . app (lift sub) m)
-
-  export
-  lt : FullTerm (N ~> N ~> B) [<]
-  lt = abs' (S Z) (\m => app (lift le) (suc m))
-
-  export
-  cond :
-    {ctx : SnocList Ty} ->
-    {ty : Ty} ->
-    List (FullTerm N ctx, FullTerm (N ~> ty) ctx) ->
-    FullTerm (N ~> ty) ctx
-  cond [] = lift arb
-  cond ((n, v) :: xs) =
-    abs' (S Z)
-      (\t =>
-        app' (lift if')
-          [<app' (lift le) [<t, drop n]
-          , app (drop v) t
-          , app (drop $ cond xs) (app' (lift sub) [<t, drop n])])
-
-namespace Data
-  public export
-  Shape : Type
-  Shape = (Ty, Nat)
-
-  public export
-  Container : Type
-  Container = List1 Shape
-
-  public export
-  fillShape : Shape -> Ty -> Ty
-  fillShape (shape,  n) ty = shape * Vect n ty
-
-  public export
-  fill : Container -> Ty -> Ty
-  fill c ty = Sum (map (flip fillShape ty) c)
-
-  export
-  fix : Container -> Ty
-  fix c = Product [<N, N ~> N, N ~> fill c N]
-  --                ^  ^       ^- tags and next positions
-  --                |  |- offset
-  --                |- pred (number of tags in structure)
-
-  mapShape :
-    {shape : Shape} ->
-    {ty, ty' : Ty} ->
-    FullTerm ((ty ~> ty') ~> fillShape shape ty ~> fillShape shape ty') [<]
-  mapShape {shape = (shape, n)} = mapSnd . mapVect
-
-  gmap :
-    {0 f : a -> b} ->
-    {0 P : a -> Type} ->
-    {0 Q : b -> Type} ->
-    ({x : a} -> P x -> Q (f x)) ->
-    {xs : List a} ->
-    All P xs ->
-    All Q (map f xs)
-  gmap f [] = []
-  gmap f (px :: pxs) = f px :: gmap f pxs
-
-  forgetMap :
-    (0 f : a -> b) ->
-    (0 xs : List1 a) ->
-    forget (map f xs) = map f (forget xs)
-  forgetMap f (head ::: tail) = Refl
-
-  calcOffsets :
-    {ctx : SnocList Ty} ->
-    {c : Container} ->
-    {n : Nat} ->
-    (ts : FullTerm (Vect n (fix c)) ctx) ->
-    (acc : FullTerm N ctx) ->
-    List (FullTerm N ctx, FullTerm (N ~> N) ctx)
-  calcOffsets {n = 0} ts acc = []
-  calcOffsets {n = S k} ts acc =
-    let hd = app (lift head) ts in
-    let n = app (lift $ project $ There $ There Here) hd in
-    let offset = app (lift $ project $ There Here) hd in
-    (n, app (lift add) acc . offset) ::
-    calcOffsets
-      (app (lift tail) ts)
-      (app' (lift add) [<suc n, acc])
-
-  calcData :
-    {ctx : SnocList Ty} ->
-    {c : Container} ->
-    {n : Nat} ->
-    (ts : FullTerm (Vect n (fix c)) ctx) ->
-    (acc : FullTerm N ctx) ->
-    List (FullTerm N ctx, FullTerm (N ~> fill c N) ctx)
-  calcData {n = 0} ts acc = []
-  calcData {n = S k} ts acc =
-    let hd = app (lift head) ts in
-    let n = app (lift $ project $ There $ There Here) hd in
-    (n, app (lift $ project Here) hd) ::
-    calcData
-      (app (lift tail) ts)
-      (app' (lift add) [<suc n, acc])
-
-  export
-  intro :
-    {c : Container} ->
-    {shape : Shape} ->
-    Elem shape (forget c) ->
-    FullTerm (fillShape shape (fix c) ~> fix c) [<]
-  intro {shape = (shape, n)} i = abs' (S Z)
-    (\t =>
-      app' (lift $ pair' {tys = [<N, N ~> N, N ~> fill c N]})
-        [<app (lift (sum . app mapVect (abs' (S Z) suc . project (There $ There Here)) . snd)) t
-        , cond ((zero, abs' (S Z) suc) :: calcOffsets (app (lift snd) t) (suc zero))
-        , cond
-          (  (zero,
-              abs
-                (app
-                  (lift $ put {tys = map (flip fillShape N) c} $
-                    rewrite forgetMap (flip fillShape N) c in
-                    elemMap (flip fillShape N) i)
-                  (app' (lift mapSnd) [<abs (lift $ enumerate n), drop t])))
-          :: calcData (app (lift snd) t) (suc zero)
-          )
-        ])
-
-  export
-  elim :
-    {c : Container} ->
-    {ctx : SnocList Ty} ->
-    {ty : Ty} ->
-    All (flip FullTerm ctx . (~> ty) . flip Data.fillShape ty) (forget c) ->
-    FullTerm (fix c ~> ty) ctx
-  elim cases = abs' (S Z)
-    (\t =>
-      let tags = suc (app (lift $ project $ There $ There Here) t) in
-      let offset = app (lift $ project $ There Here) (drop $ drop t) in
-      let vals = app (lift $ project $ Here) (drop $ drop t) in
-      app'
-        (rec tags
-          (lift arb)
-          (abs' (S $ S Z) (\rec, n =>
-            app
-              (any {tys = map (flip fillShape N) c}
-                (rewrite forgetMap (flip fillShape N) c in
-                 gmap
-                   (\f =>
-                     drop (drop $ drop f) .
-                     app (lift mapShape) (rec . app (lift add) (app offset n)))
-                   cases) .
-               vals)
-              n)))
-        [<zero])
-
-  -- elim cases (#tags-1,offset,data) =
-  --   let
-  --       step : (N -> ty) -> (N -> ty)
-  --       step rec n =
-  --         case rec n of
-  --           i => cases(i) . mapShape (rec . (+ offset n))
-  --   in
-  --       rec #tags arb step 0
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr
deleted file mode 100644
index b088e6f..0000000
--- a/src/Total/LogRel.idr
+++ /dev/null
@@ -1,355 +0,0 @@
-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 : _} -> FullTerm ty ctx -> Type) ->
-  {ty : 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 : FullTerm ty ctx') ->
-   LogRel p u ->
-   LogRel p (app (wkn t thin) u))
-
-export
-escape :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  {ty : Ty} ->
-  {0 t : FullTerm ty ctx} ->
-  LogRel P t ->
-  P t
-escape {ty = N} pt = pt
-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
-  constructor MkPresHelper
-  0 app :
-    {ctx : SnocList Ty} ->
-    {ty, ty' : Ty} ->
-    (t, u : FullTerm (ty ~> ty') ctx) ->
-    {ctx' : SnocList Ty} ->
-    (thin : ctx `Thins` ctx') ->
-    (v : FullTerm 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} ->
-    P t ->
-    (0 _ : R t u) ->
-    P u
-
-%name PreserveHelper help
-
-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) ->
-  PreserveHelper P (flip (>) `on` CoDebruijn.toTerm)
-backStepHelper pres =
-  MkPresHelper
-    (\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 :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  {0 R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type} ->
-  {ty : 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))
-
-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 [<]
-  (:<) :
-    {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-    AllLogRel P sub ->
-    LogRel P t ->
-    AllLogRel P (sub :< t)
-
-%name AllLogRel allRels
-
-index :
-  {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 (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 : _} -> FullTerm ty ctx -> Type) ->
-  {ctx : SnocList Ty} ->
-  {ty : Ty} ->
-  (t : FullTerm ty ctx) ->
-  Type
-Valid p t =
-  {ctx' : SnocList Ty} ->
-  (sub : CoTerms ctx ctx') ->
-  (allRel : AllLogRel p sub) ->
-  LogRel p (subst t sub)
-
-public export
-record ValidHelper (P : {ctx, ty : _} -> FullTerm 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)
-  rec :
-    {ctx : SnocList Ty} ->
-    {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 : FullTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u
-  wkn : forall ctx, ctx', ty.
-    {0 t : FullTerm ty ctx} ->
-    P t ->
-    (thin : ctx `Thins` ctx') ->
-    P (wkn t thin)
-
-%name ValidHelper help
-
-wknRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  ValidHelper P ->
-  {ty : 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
-  )
-
-wknAllRel :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  ValidHelper P ->
-  {ctx : SnocList Ty} ->
-  {sub : CoTerms ctx ctx'} ->
-  AllLogRel P sub ->
-  (thin : ctx' `Thins` ctx'') ->
-  AllLogRel P (wknAll sub thin)
-wknAllRel help [<] thin = [<]
-wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin
-
-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 ->
-  {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'
-  )
-
-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
-  help.suc pt
-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 :
-  {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} ->
-  {ctx : SnocList Ty} ->
-  {ty : Ty} ->
-  ValidHelper P ->
-  (t : FullTerm ty ctx) ->
-  P t
-allRel help t =
-  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
deleted file mode 100644
index a7aba57..0000000
--- a/src/Total/NormalForm.idr
+++ /dev/null
@@ -1,187 +0,0 @@
-module Total.NormalForm
-
-import Total.LogRel
-import Total.Reduction
-import Total.Term
-import Total.Term.CoDebruijn
-
-%prefix_record_projections off
-
-public export
-data Neutral' : CoTerm ty ctx -> Type
-public export
-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
-  WrapNe : Neutral' t -> Neutral (t `Over` thin)
-
-data Normal where
-  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 : FullTerm ty ctx) where
-  constructor MkNf
-  term : FullTerm ty ctx
-  0 steps : toTerm t >= toTerm term
-  0 normal : Normal term
-
-%name NormalForm nf
-
--- Strong Normalization Proof --------------------------------------------------
-
-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 x) -> Neutral' (Rec x)
-invRec (Ntrl n) = n
-
-invSuc : Normal' (Suc t) -> Normal' t
-invSuc (Suc n) = n
-
-wknNe : Neutral t -> Neutral (wkn t thin)
-wknNe (WrapNe n) = WrapNe n
-
-wknNf : Normal t -> Normal (wkn t thin)
-wknNf (WrapNf n) = WrapNf n
-
-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 : FullTerm ty ctx} ->
-  LogRel (\t => NormalForm t) t ->
-  (0 _ : toTerm u >= toTerm t) ->
-  LogRel (\t => NormalForm t) u
-backStepsRel =
-  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 {thin} (WrapNe {thin = thin'} n)) (escape rel).normal))
-      ?appCong2Steps
-  )
-
-recNf'' :
-  {ctx : SnocList Ty} ->
-  {ty : Ty} ->
-  {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 `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 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 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 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 : 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)
-recNf nf relU relV =
-  backStepsRel
-    (recNf' nf.term nf.normal relU relV)
-    ?recCong1Steps
-
-helper : ValidHelper (\t => NormalForm t)
-helper = MkValidHelper
-  { 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 (wknNf nf.normal)
-  }
-
-export
-normalize : {ctx : SnocList Ty} -> {ty : Ty} -> (t : FullTerm ty ctx) -> NormalForm t
-normalize = allRel helper
diff --git a/src/Total/Pretty.idr b/src/Total/Pretty.idr
deleted file mode 100644
index eade721..0000000
--- a/src/Total/Pretty.idr
+++ /dev/null
@@ -1,163 +0,0 @@
-module Total.Pretty
-
-import public Text.PrettyPrint.Prettyprinter
-import public Text.PrettyPrint.Prettyprinter.Render.Terminal
-
-import Data.DPair
-import Data.Fin
-import Data.Fin.Extra
-import Data.Nat
-import Data.Stream
-import Data.String
-
-import Total.Syntax
-import Total.Term
-
-data Syntax = Bound | Keyword
-
-keyword : Doc Syntax -> Doc Syntax
-keyword = annotate Keyword
-
-bound : Doc Syntax -> Doc Syntax
-bound = annotate Bound
-
-rec_ : Doc Syntax
-rec_ = keyword "rec"
-
-plus : Doc Syntax
-plus = keyword "+"
-
-arrow : Doc Syntax
-arrow = keyword "=>"
-
-public export
-interface Renderable (0 a : Type) where
-  fromSyntax : Syntax -> a
-
-export
-Renderable AnsiStyle where
-  fromSyntax Bound    = italic
-  fromSyntax Keyword  = color BrightWhite
-
-startPrec, leftAppPrec, appPrec : Prec
-startPrec = Open
-leftAppPrec = Equal
-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 (Abs t) =
-    let Evidence _ (len, t') = getLamNames (S len) t in
-    parenthesise (d > startPrec) $ group $ align $ hang 2 $
-      backslash <+> prettyBindings len <++> arrow <+> line <+>
-        (prettyTerm len Open (assert_smaller t t'))
-    where
-    getLamNames :
-      forall ctx, ty.
-      Len ctx ->
-      Term ctx ty ->
-      Exists {type = Pair _ _} (\ctxTy => (Len (fst ctxTy), Term (fst ctxTy) (snd ctxTy)))
-    getLamNames k (Abs t) = getLamNames (S k) t
-    getLamNames k t@(Var _) = Evidence (_, _) (k, t)
-    getLamNames k t@(App _ _) = Evidence (_, _) (k, t)
-    getLamNames k t@Zero = Evidence (_, _) (k, t)
-    getLamNames k t@(Suc _) = Evidence (_, _) (k, t)
-    getLamNames k t@(Rec _ _ _) = Evidence (_, _) (k, t)
-
-    prettyBindings' : Nat -> Nat -> Doc Syntax
-    prettyBindings' offset 0 = neutral
-    prettyBindings' offset 1 = bound (pretty $ index offset names)
-    prettyBindings' offset (S (S k)) =
-      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))
-  prettyTerm len d app@(App t u) =
-    let (f, ts) = getSpline t [prettyArg u] in
-    parenthesise (d >= appPrec) $ group $ align $ hang 2 $
-      f <+> line <+> vsep ts
-    where
-    prettyArg : forall ty. Term ctx ty -> Doc Syntax
-    prettyArg v = prettyTerm len appPrec (assert_smaller app v)
-
-    getSpline :
-      forall ty, ty'.
-      Term ctx (ty ~> ty') ->
-      List (Doc Syntax) ->
-      (Doc Syntax, List (Doc Syntax))
-    getSpline (App t u) xs = getSpline t (prettyArg u :: xs)
-    getSpline (Rec t u v) xs = (rec_ <++> prettyArg t, prettyArg u :: prettyArg v :: xs)
-    getSpline t'@(Var _) xs = (prettyTerm len leftAppPrec (assert_smaller t t'), xs)
-    getSpline t'@(Abs _) xs = (prettyTerm len leftAppPrec (assert_smaller t t'), xs)
-  prettyTerm len d Zero = pretty 0
-  prettyTerm len d (Suc t) = 
-    let (lit, t') = getSucs t in
-    case t' of
-      Just t' =>
-        parenthesise (d >= appPrec) $ group $
-          pretty (S lit) <++> plus <++> prettyTerm len leftAppPrec (assert_smaller t t')
-      Nothing => pretty (S lit)
-    where
-    getSucs : Term ctx N -> (Nat, Maybe (Term ctx N))
-    getSucs Zero = (0, Nothing)
-    getSucs (Suc t) = mapFst S (getSucs t)
-    getSucs t@(Var _) = (0, Just t)
-    getSucs t@(App _ _) = (0, Just t)
-    getSucs t@(Rec _ _ _) = (0, Just t)
-  prettyTerm len d (Rec t u v) =
-    parenthesise (d >= appPrec) $ group $ align $ hang 2 $
-      rec_ <++>
-      prettyTerm len appPrec t <+> line <+>
-      prettyTerm len appPrec u <+> line <+>
-      prettyTerm len appPrec v
-
-finToChar : Fin 26 -> Char
-finToChar 0 = 'x'
-finToChar 1 = 'y'
-finToChar 2 = 'z'
-finToChar 3 = 'a'
-finToChar 4 = 'b'
-finToChar 5 = 'c'
-finToChar 6 = 'd'
-finToChar 7 = 'e'
-finToChar 8 = 'f'
-finToChar 9 = 'g'
-finToChar 10 = 'h'
-finToChar 11 = 'i'
-finToChar 12 = 'j'
-finToChar 13 = 'k'
-finToChar 14 = 'l'
-finToChar 15 = 'm'
-finToChar 16 = 'n'
-finToChar 17 = 'o'
-finToChar 18 = 'p'
-finToChar 19 = 'q'
-finToChar 20 = 'r'
-finToChar 21 = 's'
-finToChar 22 = 't'
-finToChar 23 = 'u'
-finToChar 24 = 'v'
-finToChar 25 = 'w'
-
-name : Nat -> List Char
-name k =
-  case divMod k 26 of
-    Fraction k 26 0 r prf => [finToChar r]
-    Fraction k 26 (S q) r prf => finToChar r :: name (assert_smaller k q)
-
-export
-canonicalNames : Stream String
-canonicalNames = map (fastPack . name) nats
-
-export
-pretty : Renderable ann => (len : Len ctx) => Term ctx ty -> Doc ann
-pretty t = map fromSyntax (prettyTerm canonicalNames len Open t)
-
--- \x, y, z =>
---   rec z
---     (\a, b => \c => \d => d (\d => d c) a x)
---     (\a => \b => b y)
---     0
---     (\x => x)
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
deleted file mode 100644
index a424515..0000000
--- a/src/Total/Reduction.idr
+++ /dev/null
@@ -1,114 +0,0 @@
-module Total.Reduction
-
-import Syntax.PreorderReasoning
-import Total.Term
-
-public export
-data (>) : Term ctx ty -> Term ctx ty -> Type where
-  AbsCong : t > u -> Abs t > Abs u
-  AppCong1 : t > u -> App t v > App u v
-  AppCong2 : u > v -> App t u > App t v
-  AppBeta :
-    (0 len : Len ctx) ->
-    App (Abs t) u > subst t (Base (id @{len}) :< u)
-  SucCong : t > u -> Suc t > Suc u
-  RecCong1 : t1 > t2 -> Rec t1 u v > Rec t2 u v
-  RecCong2 : u1 > u2 -> Rec t u1 v > Rec t u2 v
-  RecCong3 : v1 > v2 -> Rec t u v1 > Rec t u v2
-  RecZero : Rec Zero u v > u
-  RecSuc : Rec (Suc t) u v > App v (Rec t u v)
-
-%name Reduction.(>) step
-
-public export
-data (>=) : Term ctx ty -> Term ctx ty -> Type where
-  Lin : t >= t
-  (:<) : t >= u -> u > v -> t >= v
-
-%name Reduction.(>=) steps
-
-export
-(++) : t >= u -> u >= v -> t >= v
-steps ++ [<] = steps
-steps ++ steps' :< step = (steps ++ steps') :< step
-
-export
-AbsCong' : t >= u -> Abs t >= Abs u
-AbsCong' [<] = [<]
-AbsCong' (steps :< step) = AbsCong' steps :< AbsCong step
-
-export
-AppCong1' : t >= u -> App t v >= App u v
-AppCong1' [<] = [<]
-AppCong1' (steps :< step) = AppCong1' steps :< AppCong1 step
-
-export
-AppCong2' : u >= v -> App t u >= App t v
-AppCong2' [<] = [<]
-AppCong2' (steps :< step) = AppCong2' steps :< AppCong2 step
-
-export
-SucCong' : t >= u -> Suc t >= Suc u
-SucCong' [<] = [<]
-SucCong' (steps :< step) = SucCong' steps :< SucCong step
-
-export
-RecCong1' : t1 >= t2 -> Rec t1 u v >= Rec t2 u v
-RecCong1' [<] = [<]
-RecCong1' (steps :< step) = RecCong1' steps :< RecCong1 step
-
-export
-RecCong2' : u1 >= u2 -> Rec t u1 v >= Rec t u2 v
-RecCong2' [<] = [<]
-RecCong2' (steps :< step) = RecCong2' steps :< RecCong2 step
-
-export
-RecCong3' : v1 >= v2 -> Rec t u v1 >= Rec t u v2
-RecCong3' [<] = [<]
-RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step
-
--- Properties ------------------------------------------------------------------
-
-lemma :
-  (t : Term (ctx :< ty) 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)
-
-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 (SucCong step) = SucCong (wknStep step)
-wknStep (RecCong1 step) = RecCong1 (wknStep step)
-wknStep (RecCong2 step) = RecCong2 (wknStep step)
-wknStep (RecCong3 step) = RecCong3 (wknStep step)
-wknStep RecZero = RecZero
-wknStep RecSuc = RecSuc
-
-export
-wknSteps : t >= u -> wkn t thin >= wkn u thin
-wknSteps [<] = [<]
-wknSteps (steps :< step) = wknSteps steps :< wknStep step
diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
deleted file mode 100644
index fead586..0000000
--- a/src/Total/Syntax.idr
+++ /dev/null
@@ -1,128 +0,0 @@
-module Total.Syntax
-
-import public Data.List
-import public Data.List.Quantifiers
-import public Data.SnocList
-import public Data.SnocList.Quantifiers
-import public Total.Term
-import public Total.Term.CoDebruijn
-
-infixr 20 ~>*
-infixl 9 .~, .*
-
-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)
-
-export
-lit : Len ctx => 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)) ->
-  FullTerm (tys ~>* ty) ctx
-absHelper Z x = x
-absHelper (S k) x =
-  absHelper k $
-  after k (\f => CoDebruijn.abs (f SnocList.Elem.Here)) $
-  before k SnocList.Elem.There x
-
-export
-abs' :
-  (len : Len ctx) =>
-  (k : Len tys) ->
-  Fun k (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
-  FullTerm (tys ~>* ty) ctx
-abs' k = absHelper k . before k (var @{lenAppend len k})
-
-export
-app' :
-  {tys : SnocList Ty} ->
-  FullTerm (tys ~>* ty) ctx ->
-  All (flip FullTerm ctx) tys ->
-  FullTerm ty ctx
-app' t [<] = t
-app' t (us :< u) = app (app' t us) u
-
--- export
--- compose :
---   {ty, ty' : Ty} ->
---   (t : FullTerm (ty' ~> ty'') ctx) ->
---   (u : FullTerm (ty ~> ty') ctx) ->
---   Len u.support =>
---   Covering Covers t.thin u.thin ->
---   CoTerm (ty ~> ty'') ctx
--- compose (t `Over` thin1) (u `Over` thin2) cover =
---   Abs
---     (MakeBound
---       (App
---         (MakePair
---           (t `Over` Drop thin1)
---           (App
---             (MakePair
---               (u `Over` Drop id)
---               (Var `Over` Keep empty)
---               (DropKeep (coverIdLeft empty)))
---            `Over` Keep thin2)
---           (DropKeep cover)))
---       (Keep Empty))
-
--- export
--- (.~) :
---   Len ctx =>
---   {ty, ty' : Ty} ->
---   CoTerm (ty' ~> ty'') ctx ->
---   CoTerm (ty ~> ty') ctx ->
---   CoTerm (ty ~> ty'') ctx
--- t .~ u = compose (t `Over` id) (u `Over` id) (coverIdLeft id)
-
-export
-(.) :
-  Len ctx =>
-  {ty, ty' : Ty} ->
-  FullTerm (ty' ~> ty'') ctx ->
-  FullTerm (ty ~> ty') ctx ->
-  FullTerm (ty ~> ty'') ctx
-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 ->
-  FullTerm (tys ~>* ty) ctx ->
-  FullTerm (tys ~>* ty') ctx
-(.*) {tys = [<]} t u = app t u
-(.*) {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))
-
-export
-id : FullTerm (ty ~> ty) [<]
-id = id' `Over` empty
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
deleted file mode 100644
index 129662a..0000000
--- a/src/Total/Term.idr
+++ /dev/null
@@ -1,357 +0,0 @@
-module Total.Term
-
-import public Data.SnocList.Elem
-import public Thinning
-import Syntax.PreorderReasoning
-
-%prefix_record_projections off
-
-infixr 10 ~>
-
-public export
-data Ty : Type where
-  N : Ty
-  (~>) : Ty -> Ty -> Ty
-
-%name Ty ty
-
-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
-
-%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)
-
-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)
-
-%name Terms sub
-
-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
-
-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
-
-public export
-subst : Len ctx' => Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
-subst (Var i) sub = index sub i
-subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop id) :< Var Here)
-subst (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
-
-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
-
--- 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)
-
-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)
-
--- Substitution & Weakening
-
-export
-wknSubst :
-  (t : Term ctx ty) ->
-  (sub : Terms ctx' ctx) ->
-  (thin : ctx' `Thins` ctx'') ->
-  wkn (subst t sub) thin = subst t (wknAll sub thin)
-wknSubst (Var i) sub thin =
-  sym (indexWknAll sub thin i)
-wknSubst (Abs 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))
-wknSubst (App t u) sub thin =
-  cong2 App (wknSubst t sub thin) (wknSubst u sub thin)
-wknSubst Zero sub thin =
-  Refl
-wknSubst (Suc t) sub thin =
-  cong Suc (wknSubst t sub thin)
-wknSubst (Rec t u v) sub thin =
-  cong3 Rec (wknSubst t sub thin) (wknSubst u sub thin) (wknSubst v sub thin)
-
-export
-substWkn :
-  (t : Term ctx ty) ->
-  (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 =
-  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
deleted file mode 100644
index 0efcdbb..0000000
--- a/src/Total/Term/CoDebruijn.idr
+++ /dev/null
@@ -1,317 +0,0 @@
-module Total.Term.CoDebruijn
-
-import public Data.SnocList.Elem
-import public Thinning
-import Syntax.PreorderReasoning
-import Total.Term
-
-%prefix_record_projections off
-
--- 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
-
-%name CoTerm t, u, v
-
-public export
-FullTerm : Ty -> SnocList Ty -> Type
-FullTerm ty ctx = Thinned (CoTerm ty) ctx
-
--- Smart Constructors ----------------------------------------------------------
-
-public export
-var : Len ctx => Elem ty ctx -> FullTerm 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)
-
-public export
-app : {ty : Ty} -> FullTerm (ty ~> ty') ctx -> FullTerm ty ctx -> FullTerm ty' ctx
-app t u = map App (MkPair t u)
-
-public export
-zero : Len ctx => FullTerm N ctx
-zero = Zero `Over` empty
-
-public export
-suc : FullTerm N ctx -> FullTerm N ctx
-suc = map Suc
-
-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)
-
--- Substitutions ---------------------------------------------------------------
-
-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
-
-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
-
-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' 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))
-
--- 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))
-
-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 = 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)