Reset using only co-de Bruijn syntax.

13 files changed, 822 insertions, 2308 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index 2456685..54b7dcc 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -8,11 +8,3 @@ depends = contrib
 
 modules
   = Thinning
-  , Total.Encoded.Util
-  , Total.LogRel
-  , Total.NormalForm
-  , Total.Pretty
-  , Total.Reduction
-  , Total.Syntax
-  , Total.Term
-  , Total.Term.CoDebruijn
diff --git a/src/Term.idr b/src/Term.idr
new file mode 100644
index 0000000..e9f6b1f
--- /dev/null
+++ b/src/Term.idr
@@ -0,0 +1,341 @@
+module Term
+
+import Control.Order
+import Control.Relation
+import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Generic
+
+import public Data.SnocList.Quantifiers
+import public Thinned
+import public Type
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+||| System T terms that use all the variables in scope.
+public export
+data FullTerm : Ty -> SnocList Ty -> Type where
+  Var : FullTerm ty [<ty]
+  Const : FullTerm ty' ctx -> FullTerm (ty ~> ty') ctx
+  Abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx
+  App :
+    {ty : Ty} ->
+    Pair (FullTerm (ty ~> ty')) (FullTerm ty) ctx ->
+    FullTerm ty' ctx
+  Zero : FullTerm N [<]
+  Suc : FullTerm N ctx -> FullTerm N ctx
+  Rec :
+    Pair (FullTerm N) (Pair (FullTerm ty) (FullTerm (ty ~> ty))) ctx ->
+    FullTerm ty ctx
+
+%name FullTerm t, u, v
+
+||| System T terms.
+public export
+Term : Ty -> SnocList Ty -> Type
+Term ty ctx = Thinned (FullTerm ty) ctx
+
+-- Smart Constructors ----------------------------------------------------------
+
+namespace Smart
+  export
+  Var : Elem ty ctx -> Term ty ctx
+  Var i = Var `Over` Point i
+
+  export
+  Const : Term ty' ctx -> Term (ty ~> ty') ctx
+  Const t = map Const t
+
+  export
+  Abs : Term ty' (ctx :< ty) -> Term (ty ~> ty') ctx
+  Abs (t `Over` Id) = Abs t `Over` Id
+  Abs (t `Over` Empty) = Const t `Over` Empty
+  Abs (t `Over` Drop thin) = Const t `Over` thin
+  Abs (t `Over` Keep thin) = Abs t `Over` thin
+
+  export
+  App : {ty : Ty} -> Term (ty ~> ty') ctx -> Term ty ctx -> Term ty' ctx
+  App t u = map App $ MkPair t u
+
+  export
+  Zero : Term N ctx
+  Zero = Zero `Over` Empty
+
+  export
+  Suc : Term N ctx -> Term N ctx
+  Suc t = map Suc t
+
+  export
+  Rec : Term N ctx -> Term ty ctx -> Term (ty ~> ty) ctx -> Term ty ctx
+  Rec t u v = map Rec $ MkPair t (MkPair u v)
+
+  --- Properties
+
+  export
+  varCong : {0 i, j : Elem ty ctx} -> i = j -> Var i <~> Var j
+
+  export
+  shiftVar : (i : Elem ty ctx) -> shift (Var i) <~> Var (There i)
+
+  export
+  constCong : {0 t, u : Term ty' ctx} -> t <~> u -> Const t <~> Const u
+
+  export
+  absCong : {0 t, u : Term ty' (ctx :< ty)} -> t <~> u -> Abs t <~> Abs u
+
+  export
+  appCong :
+    {0 t1, u1 : Term (ty ~> ty') ctx} ->
+    {0 t2, u2 : Term ty ctx} ->
+    t1 <~> u1 ->
+    t2 <~> u2 ->
+    App t1 t2 <~> App u1 u2
+
+  export
+  sucCong : {0 t, u : Term N ctx} -> t <~> u -> Suc t <~> Suc u
+
+  export
+  recCong :
+    {0 t1, u1 : Term N ctx} ->
+    {0 t2, u2 : Term ty ctx} ->
+    {0 t3, u3 : Term (ty ~> ty) ctx} ->
+    t1 <~> u1 ->
+    t2 <~> u2 ->
+    t3 <~> u3 ->
+    Rec t1 t2 t3 <~> Rec u1 u2 u3
+  recCong prf1 prf2 prf3 =
+    mapCong Rec
+      ?recCong_rhs_1
+
+-- Substitution Definition -----------------------------------------------------
+
+||| Substitution of variables for terms.
+public export
+data Subst : (ctx, ctx' : SnocList Ty) -> Type where
+  Base : ctx `Thins` ctx' -> Subst ctx ctx'
+  (:<) : Subst ctx ctx' -> Term ty ctx' -> Subst (ctx :< ty) ctx'
+
+%name Subst sub
+
+export
+index : Subst ctx ctx' -> Elem ty ctx -> Term ty ctx'
+index (Base thin) i = Var (index thin i)
+index (sub :< v) Here = v
+index (sub :< v) (There i) = index sub i
+
+||| Equivalence relation on substitutions.
+public export
+record (<~>) (sub1, sub2 : Subst ctx ctx') where
+  constructor MkEquivalence
+  equiv : forall ty. (i : Elem ty ctx) -> index sub1 i <~> index sub2 i
+
+%name Term.(<~>) prf
+
+--- Properties
+
+export
+irrelevantEquiv :
+  {0 sub1, sub2 : Subst ctx ctx'} ->
+  (0 prf : sub1 <~> sub2) ->
+  sub1 <~> sub2
+irrelevantEquiv prf = MkEquivalence (\i => irrelevantEquiv $ prf.equiv i)
+
+export
+Reflexive (Subst ctx ctx') (<~>) where
+  reflexive = MkEquivalence (\i => reflexive)
+
+export
+Symmetric (Subst ctx ctx') (<~>) where
+  symmetric prf = MkEquivalence (\i => symmetric $ prf.equiv i)
+
+export
+Transitive (Subst ctx ctx') (<~>) where
+  transitive prf1 prf2 = MkEquivalence (\i => transitive (prf1.equiv i) (prf2.equiv i))
+
+export
+Equivalence (Subst ctx ctx') (<~>) where
+
+export
+Preorder (Subst ctx ctx') (<~>) where
+
+namespace Subst
+  export
+  Base :
+    {0 thin1, thin2 : ctx `Thins` ctx'} ->
+    thin1 <~> thin2 ->
+    Base thin1 <~> Base thin2
+  Base prf = MkEquivalence (\i => varCong (prf.equiv i))
+
+  export
+  (:<) :
+    {0 sub1, sub2 : Subst ctx ctx'} ->
+    {0 t, u : Term ty ctx'} ->
+    sub1 <~> sub2 ->
+    t <~> u ->
+    sub1 :< t <~> sub2 :< u
+  prf1 :< prf2 =
+    MkEquivalence (\i => case i of Here => prf2; There i => prf1.equiv i)
+
+-- Operations ------------------------------------------------------------------
+
+||| Shifts a substitution under a binder.
+export
+shift : Subst ctx ctx' -> Subst ctx (ctx' :< ty)
+shift (Base thin) = Base (Drop thin)
+shift (sub :< t) = shift sub :< shift t
+
+||| Lifts a substitution under a binder.
+export
+lift : Subst ctx ctx' -> Subst (ctx :< ty) (ctx' :< ty)
+lift sub = shift sub :< Var Here
+
+||| Limits the domain of a substitution
+export
+(.) : Subst ctx' ctx'' -> ctx `Thins` ctx' -> Subst ctx ctx''
+Base thin' . thin = Base (thin' . thin)
+(sub :< t) . Id = sub :< t
+(sub :< t) . Empty = Base Empty
+(sub :< t) . Drop thin = sub . thin
+(sub :< t) . Keep thin = sub . thin :< t
+
+--- Properties
+
+export
+shiftIndex :
+  (sub : Subst ctx ctx') ->
+  (i : Elem ty ctx) ->
+   shift (index sub i) <~> index (shift sub) i
+shiftIndex (Base thin) i = CalcWith $
+  |~ shift (Var $ index thin i)
+  <~ Var (There $ index thin i) ...(shiftVar (index thin i))
+  <~ Var (index (Drop thin) i)  ..<(varCong $ indexDrop thin i)
+shiftIndex (sub :< v) Here = reflexive
+shiftIndex (sub :< v) (There i) = shiftIndex sub i
+
+export
+shiftCong : {0 sub1, sub2 : Subst ctx' ctx''} -> sub1 <~> sub2 -> shift sub1 <~> shift sub2
+shiftCong prf = irrelevantEquiv $ MkEquivalence (\i =>
+  CalcWith $
+    |~ index (shift sub1) i
+    <~ shift (index sub1 i) ..<(shiftIndex sub1 i)
+    <~ shift (index sub2 i) ...(shiftCong (prf.equiv i))
+    <~ index (shift sub2) i ...(shiftIndex sub2 i))
+
+export
+liftCong : {0 sub1, sub2 : Subst ctx' ctx''} -> sub1 <~> sub2 -> lift sub1 <~> lift sub2
+liftCong prf = shiftCong prf :< (irrelevantEquiv $ reflexive)
+
+export
+indexHomo :
+  (sub : Subst ctx' ctx'') ->
+  (thin : ctx `Thins` ctx') ->
+  (i : Elem ty ctx) ->
+  index sub (index thin i) = index (sub . thin) i
+indexHomo (Base thin') thin i = cong Var (indexHomo thin' thin i)
+indexHomo (sub :< v) Id i = cong (index (sub :< v)) $ indexId i
+indexHomo (sub :< v) (Drop thin) i = Calc $
+  |~ index (sub :< v) (index (Drop thin) i)
+  ~~ index (sub :< v) (There (index thin i)) ...(cong (index (sub :< v)) $ indexDrop thin i)
+  ~~ index sub (index thin i)                ...(Refl)
+  ~~ index (sub . thin) i                    ...(indexHomo sub thin i)
+indexHomo (sub :< v) (Keep thin) Here = Calc $
+  |~ index (sub :< v) (index (Keep thin) Here)
+  ~~ index (sub :< v) Here                     ...(cong (index (sub :< v)) $ indexKeepHere thin)
+  ~~ v                                         ...(Refl)
+indexHomo (sub :< v) (Keep thin) (There i) = Calc $
+  |~ index (sub :< v) (index (Keep thin) (There i))
+  ~~ index (sub :< v) (There (index thin i))       ...(cong (index (sub :< v)) $ indexKeepThere thin i)
+  ~~ index sub (index thin i)                      ...(Refl)
+  ~~ index (sub . thin) i                          ...(indexHomo sub thin i)
+
+export
+compCong :
+  {0 sub1, sub2 : Subst ctx' ctx''} ->
+  {0 thin1, thin2 : ctx `Thins` ctx'} ->
+  sub1 <~> sub2 ->
+  thin1 <~> thin2 ->
+  (sub1 . thin1) <~> (sub2 . thin2)
+compCong prf1 prf2 = irrelevantEquiv $ MkEquivalence (\i => CalcWith $
+  |~ index (sub1 . thin1) i
+  ~~ index sub1 (index thin1 i) ..<(indexHomo sub1 thin1 i)
+  <~ index sub2 (index thin1 i) ...(prf1.equiv (index thin1 i))
+  ~~ index sub2 (index thin2 i) ...(cong (index sub2) $ prf2.equiv i)
+  ~~ index (sub2 . thin2) i     ...(indexHomo sub2 thin2 i))
+
+-- Substitution Operation ------------------------------------------------------
+
+fullSubst : FullTerm ty ctx -> Subst ctx ctx' -> Term ty ctx'
+fullSubst Var sub = index sub Here
+fullSubst (Const t) sub = Const (fullSubst t sub)
+fullSubst (Abs t) sub = Abs (fullSubst t $ lift sub)
+fullSubst (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) sub =
+  App (fullSubst t $ sub . thin1) (fullSubst u $ sub . thin2)
+fullSubst Zero sub = Zero
+fullSubst (Suc t) sub = Suc (fullSubst t sub)
+fullSubst
+  (Rec (MakePair
+    (t `Over` thin1)
+    (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin')
+    _))
+  sub =
+  let sub' = sub . thin' in
+  Rec
+    (fullSubst t $ sub . thin1)
+    (fullSubst u $ sub' . thin2)
+    (fullSubst v $ sub' . thin3)
+
+||| Applies a substitution to a term.
+export
+subst : Term ty ctx -> Subst ctx ctx' -> Term ty ctx'
+subst (t `Over` thin) sub = fullSubst t (sub . thin)
+
+--- Properties
+
+fullSubstCong :
+  (t : FullTerm ty ctx) ->
+  {0 sub1, sub2 : Subst ctx ctx'} ->
+  sub1 <~> sub2 ->
+  fullSubst t sub1 <~> fullSubst t sub2
+fullSubstCong Var prf = prf.equiv Here
+fullSubstCong (Const t) prf = constCong (fullSubstCong t prf)
+fullSubstCong (Abs t) prf = absCong (fullSubstCong t $ liftCong prf)
+fullSubstCong (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) prf =
+  appCong
+    (fullSubstCong t $ compCong prf reflexive)
+    (fullSubstCong u $ compCong prf reflexive)
+fullSubstCong Zero prf = irrelevantEquiv $ reflexive
+fullSubstCong (Suc t) prf = sucCong (fullSubstCong t prf)
+fullSubstCong
+  (Rec (MakePair
+    (t `Over` thin1)
+    (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin')
+    _))
+  prf =
+  let prf' = compCong prf reflexive in
+  recCong
+    (fullSubstCong t $ compCong prf reflexive)
+    (fullSubstCong u $ compCong prf' reflexive)
+    (fullSubstCong v $ compCong prf' reflexive)
+
+export
+substCong :
+  {0 t, u : Term ty ctx} ->
+  {0 sub1, sub2 : Subst ctx ctx'} ->
+  t <~> u ->
+  sub1 <~> sub2 ->
+  subst t sub1 <~> subst u sub2
+substCong (UpToThin prf1) prf2 = irrelevantEquiv $ fullSubstCong _ (compCong prf2 prf1)
+
+export
+substBase :
+  (t : Term ty ctx) ->
+  (thin : ctx `Thins` ctx') ->
+  subst t (Base thin) <~> wkn t thin
+
+export
+substHomo :
+  (t : Term ty ctx) ->
+  (sub1 : Subst ctx ctx') ->
+  (sub2 : Subst ctx' ctx'') ->
+  subst (subst t sub1) sub2 <~> subst t ?d
diff --git a/src/Thinned.idr b/src/Thinned.idr
new file mode 100644
index 0000000..7f5d2ac
--- /dev/null
+++ b/src/Thinned.idr
@@ -0,0 +1,140 @@
+module Thinned
+
+import Control.Order
+import Control.Relation
+
+import public Thinning
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+||| Data embedded in a wider context via a thinning.
+public export
+record Thinned (t : SnocList a -> Type) (sx : SnocList a) where
+  constructor Over
+  {0 support : SnocList a}
+  value : t support
+  thin : support `Thins` sx
+
+%name Thinned v, u
+
+||| An equivalence relation on thinned objects.
+public export
+data (<~>) : Thinned t sx -> Thinned t sx -> Type where
+  UpToThin :
+    {0 v : t sx} ->
+    {0 thin1, thin2 : sx `Thins` sy} ->
+    thin1 <~> thin2 ->
+    (<~>) {t} (v `Over` thin1) (v `Over` thin2)
+
+%name Thinned.(<~>) prf
+
+export (.supportPrf) :
+  {0 v, u : Thinned t sx} ->
+  v <~> u ->
+  v.support = u.support
+(UpToThin prf) .supportPrf = Refl
+
+export (.valuePrf) :
+  {0 v, u : Thinned t sx} ->
+  (e : v <~> u) ->
+  v.value = (rewrite e.supportPrf in u.value)
+(UpToThin prf) .valuePrf = Refl
+
+export (.thinPrf) :
+  {0 v, u : Thinned t sx} ->
+  (e : v <~> u) ->
+  v.thin <~> (rewrite e.supportPrf in u.thin)
+(UpToThin prf) .thinPrf = prf
+
+--- Properties
+
+export
+irrelevantEquiv :
+  {0 v, u : Thinned t sx} ->
+  (0 prf : v <~> u) ->
+  v <~> u
+irrelevantEquiv {v = v `Over` thin1, u = u `Over` thin2} prf =
+  rewrite prf.supportPrf in
+  rewrite prf.valuePrf in
+  UpToThin (rewrite sym prf.supportPrf in irrelevantEquiv prf.thinPrf)
+
+export
+Reflexive (Thinned t sx) (<~>) where
+  reflexive {x = t `Over` thin} = UpToThin reflexive
+
+export
+Symmetric (Thinned t sx) (<~>) where
+  symmetric (UpToThin prf) = UpToThin (symmetric prf)
+
+export
+Transitive (Thinned t sx) (<~>) where
+  transitive (UpToThin prf1) (UpToThin prf2) = UpToThin (transitive prf1 prf2)
+
+export
+Equivalence (Thinned t sx) (<~>) where
+
+export
+Preorder (Thinned t sx) (<~>) where
+
+-- Operations ------------------------------------------------------------------
+
+||| Map the underlying value.
+public export
+map : (forall sx. t sx -> u sx) -> Thinned t sx -> Thinned u sx
+map f (value `Over` thin) = f value `Over` thin
+
+||| Weaken the surrounding context.
+public export
+wkn : Thinned t sx -> sx `Thins` sy -> Thinned t sy
+wkn (value `Over` thin') thin = value `Over` thin . thin'
+
+||| Shift the surrounding context.
+public export
+shift : Thinned t sx -> Thinned t (sx :< x)
+shift (value `Over` thin) = value `Over` Drop thin
+
+--- Properties
+
+export
+mapCong :
+  {0 t, u : SnocList a -> Type} ->
+  (0 f : forall sx. t sx -> u sx) ->
+  {0 v1, v2 : Thinned t sx} ->
+  v1 <~> v2 ->
+  map f v1 <~> map f v2
+mapCong f (UpToThin prf) = UpToThin prf
+
+export
+shiftCong : {0 v, u : Thinned t sx} -> v <~> u -> shift v <~> shift u
+shiftCong (UpToThin prf) = UpToThin (dropCong prf)
+
+-- Pairs -----------------------------------------------------------------------
+
+||| Product of two values ensuring the whole context is used.
+public export
+record Pair (t, u : SnocList a -> Type) (sx : SnocList a) where
+  constructor MakePair
+  fst : Thinned t sx
+  snd : Thinned u sx
+  0 cover : Covering fst.thin snd.thin
+
+||| Smart constructor for thinned pairs.
+export
+MkPair : Thinned t sx -> Thinned u sx -> Thinned (Pair t u) sx
+MkPair (v `Over` thin1) (u `Over` thin2) =
+  let cp = coprod thin1 thin2 in
+  MakePair (v `Over` cp.thin1') (u `Over` cp.thin2') cp.cover `Over` cp.factor
+
+--- Properties
+
+export
+mkPairCong :
+  {0 v1, w1 : Thinned t sx} ->
+  {0 v2, w2 : Thinned u sx} ->
+  v1 <~> w1 ->
+  v2 <~> w2 ->
+  MkPair v1 v2 <~> MkPair w1 w2
+mkPairCong (UpToThin prf1) (UpToThin prf2) =
+  ?mkPairCong_rhs_1
diff --git a/src/Thinning.idr b/src/Thinning.idr
index d2d65df..1ba5eb0 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -1,246 +1,187 @@
+||| A setoid of context thinnings.
 module Thinning
 
-import Data.Singleton
-import Data.SnocList.Elem
+import Control.Order
+import Control.Relation
+import Data.Either
+import Data.Nat
+import Syntax.PreorderReasoning
+
+import public Data.SnocList.Elem
 
 %prefix_record_projections off
 
+infix 4 <~>
+
 -- Definition ------------------------------------------------------------------
 
+||| An injective, order-preserving map from one context to another.
 public export
 data Thins : SnocList a -> SnocList a -> Type where
-  Empty : [<] `Thins` [<]
-  Drop : sx `Thins` sy -> sx `Thins` sy :< z
-  Keep :
-    (thin : sx `Thins` sy) ->
-    sx :< z `Thins` sy :< z
+  ||| Identity map.
+  Id : sx `Thins` sx
+  ||| Empty map.
+  Empty : [<] `Thins` sx
+  ||| Skips over an element in the target context.
+  Drop : sx `Thins` sy -> sx `Thins` sy :< y
+  ||| Extends both contexts with a new element.
+  Keep : sx `Thins` sy -> sx :< z `Thins` sy :< z
 
 %name Thins thin
 
--- Utility ---------------------------------------------------------------------
-
-public export
-data Len : SnocList a -> Type where
-  Z : Len [<]
-  S : Len sx -> Len (sx :< x)
-
-%name Len k, m, n
-
-%hint
-public export
-length : (sx : SnocList a) -> Len sx
-length [<] = Z
-length (sx :< x) = S (length sx)
-
-%hint
+||| Apply a thinning to an element of the source context.
 export
-lenAppend : Len sx -> Len sy -> Len (sx ++ sy)
-lenAppend k Z = k
-lenAppend k (S m) = S (lenAppend k m)
-
-%hint
-public export
-lenPred : Len (sx :< x) -> Len sx
-lenPred (S k) = k
-
-export
-Cast (Len sx) Nat where
-  cast Z = 0
-  cast (S k) = S (cast k)
-
--- Smart Constructors ----------------------------------------------------------
-
-export
-empty : (len : Len sx) => [<] `Thins` sx
-empty {len = Z} = Empty
-empty {len = S k} = Drop empty
-
-public export
-id : (len : Len sx) => sx `Thins` sx
-id {len = Z} = Empty
-id {len = S k} = Keep id
-
-public export
-point : Len sx => Elem ty sx -> [<ty] `Thins` sx
-point Here = Keep empty
-point (There i) = Drop (point i)
-
--- Operations ------------------------------------------------------------------
-
-public export
-index : sx `Thins` sy -> Elem z sx -> Elem z sy
+index : sx `Thins` sy -> Elem x sx -> Elem x sy
+index Id i = i
 index (Drop thin) i = There (index thin i)
 index (Keep thin) Here = Here
 index (Keep thin) (There i) = There (index thin i)
 
+||| An equivalence relation on thinnings. Two thinnings are equal if they have
+||| the same action on elements.
 public export
-(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
-Empty . thin1 = thin1
-Drop thin2 . thin1 = Drop (thin2 . thin1)
-Keep thin2 . Drop thin1 = Drop (thin2 . thin1)
-Keep thin2 . Keep thin1 = Keep (thin2 . thin1)
+record (<~>) (thin1, thin2 : sx `Thins` sy) where
+  constructor MkEquivalence
+  equiv : forall x. (i : Elem x sx) -> index thin1 i = index thin2 i
 
-export
-(++) : sx `Thins` sy -> sz `Thins` sw -> sx ++ sz `Thins` sy ++ sw
-thin2 ++ Empty = thin2
-thin2 ++ (Drop thin1) = Drop (thin2 ++ thin1)
-thin2 ++ (Keep thin1) = Keep (thin2 ++ thin1)
+%name (<~>) prf
 
--- Commuting Triangles and Coverings -------------------------------------------
+--- Properties
 
-data Triangle : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -> Type where
-  EmptyAny : Triangle Empty thin1 thin1
-  DropAny : Triangle thin2 thin1 thin -> Triangle (Drop thin2) thin1 (Drop thin)
-  KeepDrop : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Drop thin1) (Drop thin)
-  KeepKeep : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Keep thin1) (Keep thin)
+-- Relational
 
-public export
-data Overlap = Covers | Partitions
+export
+irrelevantEquiv :
+  {0 thin1, thin2 : sx `Thins` sy} ->
+  (0 prf : thin1 <~> thin2) ->
+  thin1 <~> thin2
+irrelevantEquiv prf = MkEquivalence (\i => irrelevantEq $ prf.equiv i)
 
-namespace Covering
-  public export
-  data Covering : Overlap -> sx `Thins` sz -> sy `Thins` sz -> Type where
-    EmptyEmpty : Covering ov Empty Empty
-    DropKeep : Covering ov thin1 thin2 -> Covering ov (Drop thin1) (Keep thin2)
-    KeepDrop : Covering ov thin1 thin2 -> Covering ov (Keep thin1) (Drop thin2)
-    KeepKeep : Covering Covers thin1 thin2 -> Covering Covers (Keep thin1) (Keep thin2)
+export
+Reflexive (sx `Thins` sy) (<~>) where
+  reflexive = MkEquivalence (\i => Refl)
 
-public export
-record Coproduct {sx, sy, sz : SnocList a} (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where
-  constructor MkCoprod
-  {0 sw : SnocList a}
-  {thin1' : sx `Thins` sw}
-  {thin2' : sy `Thins` sw}
-  {thin : sw `Thins` sz}
-  0 left : Triangle thin thin1' thin1
-  0 right : Triangle thin thin2' thin2
-  0 cover : Covering Covers thin1' thin2'
+export
+Symmetric (sx `Thins` sy) (<~>) where
+  symmetric prf = MkEquivalence (\i => sym $ prf.equiv i)
 
 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) =
-  { left $= DropAny, right $= DropAny } (coprod thin1 thin2)
-coprod (Drop thin1) (Keep thin2) =
-  { left $= KeepDrop, right $= KeepKeep, cover $= DropKeep } (coprod thin1 thin2)
-coprod (Keep thin1) (Drop thin2) =
-  { left $= KeepKeep, right $= KeepDrop, cover $= KeepDrop } (coprod thin1 thin2)
-coprod (Keep thin1) (Keep thin2) =
-  { left $= KeepKeep, right $= KeepKeep, cover $= KeepKeep } (coprod thin1 thin2)
+Transitive (sx `Thins` sy) (<~>) where
+  transitive prf1 prf2 = MkEquivalence (\i => trans (prf1.equiv i) (prf2.equiv i))
 
--- Splitting off Contexts ------------------------------------------------------
+export
+Equivalence (sx `Thins` sy) (<~>) where
 
-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)
+export
+Preorder (sx `Thins` sy) (<~>) where
 
-public export
-split : Len local -> (thin : sx `Thins` global ++ local) -> Split global local thin
-split Z thin = MkSplit thin Empty
-split (S k) (Drop thin) with (split k thin)
-  split (S k) (Drop .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Drop thin1)
-split (S k) (Keep thin) with (split k thin)
-  split (S k) (Keep .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Keep thin1)
+export
+dropCong : thin1 <~> thin2 -> Drop thin1 <~> Drop thin2
+dropCong prf = MkEquivalence (\i => cong There $ prf.equiv i)
 
--- Thinned Things --------------------------------------------------------------
+export
+keepCong : thin1 <~> thin2 -> Keep thin1 <~> Keep thin2
+keepCong prf = MkEquivalence
+  (\i =>
+    case i of
+      Here => Refl
+      There i => cong There $ prf.equiv i)
 
-public export
-record Thinned (T : SnocList a -> Type) (sx : SnocList a) where
-  constructor Over
-  {0 support : SnocList a}
-  value : T support
-  thin : support `Thins` sx
+-- Indexing
 
-public export
-record OverlapPair (overlap : Overlap) (T, U : SnocList a -> Type) (sx : SnocList a) where
-  constructor MakePair
-  left : Thinned T sx
-  right : Thinned U sx
-  0 cover : Covering overlap left.thin right.thin
+export
+indexId : (i : Elem x sx) -> index Id i = i
+indexId i = Refl
 
-public export
-Pair : (T, U : SnocList a -> Type) -> SnocList a -> Type
-Pair = OverlapPair Covers
+export
+indexDrop :
+  (thin : sx `Thins` sy) ->
+  (i : Elem x sx) ->
+  index (Drop thin) i = There (index thin i)
+indexDrop thin i = Refl
 
-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
-  MakePair (t `Over` cp.thin1') (u `Over` cp.thin2') cp.cover `Over` cp.thin
+export
+indexKeepHere : (thin : sx `Thins` sy) -> index (Keep thin) Here = Here
+indexKeepHere thin = Refl
 
-public export
-record Binds (local : SnocList a) (T : SnocList a -> Type) (sx : SnocList a) where
-  constructor MakeBound
-  {0 used : SnocList a}
-  value : T (sx ++ used)
-  thin : used `Thins` local
+export
+indexKeepThere :
+  (thin : sx `Thins` sy) ->
+  (i : Elem x sx) ->
+  index (Keep thin) (There i) = There (index thin i)
+indexKeepThere thin i = Refl
 
-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
+-- Other
 
-public export
-map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx
-map f (value `Over` thin) = f value `Over` thin
+thinToEmpty : sx `Thins` [<] -> sx = [<]
+thinToEmpty Id = Refl
+thinToEmpty Empty = Refl
 
-public export
-drop : Thinned t sx -> Thinned t (sx :< x)
-drop (value `Over` thin) = value `Over` Drop thin
+0 thinLen : sx `Thins` sy -> length sx `LTE` length sy
+thinLen Id = reflexive
+thinLen Empty = LTEZero
+thinLen (Drop thin) = lteSuccRight (thinLen thin)
+thinLen (Keep thin) = LTESucc (thinLen thin)
 
-public export
-wkn : Thinned t sx -> sx `Thins` sy -> Thinned t sy
-wkn (value `Over` thin) thin' = value `Over` thin' . thin
+idUnique' : (thin : sx `Thins` sx) -> (i : Elem x sx) -> index thin i = i
+idUnique' Id i = Refl
+idUnique' (Drop thin) i = void $ LTEImpliesNotGT (thinLen thin) reflexive
+idUnique' (Keep thin) Here = Refl
+idUnique' (Keep thin) (There i) = cong There $ idUnique' thin i
 
--- Properties ------------------------------------------------------------------
+export
+idUnique : (thin1, thin2 : sx `Thins` sx) -> thin1 <~> thin2
+idUnique thin1 thin2 =
+  MkEquivalence
+    (\i => trans (idUnique' thin1 i) (sym $ idUnique' thin2 i))
 
 export
-lenUnique : (k, m : Len sx) -> k = m
-lenUnique Z Z = Refl
-lenUnique (S k) (S m) = cong S (lenUnique k m)
+emptyUnique : (thin1, thin2 : [<] `Thins` sx) -> thin1 <~> thin2
+emptyUnique thin1 thin2 = MkEquivalence (\i => absurd i)
 
+-- Smart Constructors ----------------------------------------------------------
+
+||| Point map. The representable thinning of an element.
 export
-emptyUnique : (thin1, thin2 : [<] `Thins` sx) -> thin1 = thin2
-emptyUnique Empty Empty = Refl
-emptyUnique (Drop thin1) (Drop thin2) = cong Drop (emptyUnique thin1 thin2)
+Point : Elem x sx -> [<x] `Thins` sx
+Point Here = Keep Empty
+Point (There i) = Drop (Point i)
 
 export
-identityLeft : (len : Len sy) => (thin : sx `Thins` sy) -> id @{len} . thin = thin
-identityLeft {len = Z} thin = Refl
-identityLeft {len = S k} (Drop thin) = cong Drop (identityLeft thin)
-identityLeft {len = S k} (Keep thin) = cong Keep (identityLeft thin)
+indexPoint : (i : Elem x sx) -> index (Point i) Here = i
+indexPoint Here = Refl
+indexPoint (There i) = cong There $ indexPoint i
 
 export
-identityRight : (len : Len sx) => (thin : sx `Thins` sy) -> thin . id @{len} = thin
-identityRight {len = Z} Empty = Refl
-identityRight (Drop thin) = cong Drop (identityRight thin)
-identityRight {len = S k} (Keep thin) = cong Keep (identityRight thin)
+pointCong : {0 i, j : Elem x sx} -> i = j -> Point i <~> Point j
+pointCong prf = MkEquivalence (\Here => cong (\i => index (Point i) Here) prf)
 
 export
-identitySquared : (len : Len sx) -> id @{len} . id @{len} = id @{len}
-identitySquared Z = Refl
-identitySquared (S k) = cong Keep (identitySquared k)
+dropPoint : (i : Elem x sx) -> Drop (Point i) <~> Point (There i)
+dropPoint i = MkEquivalence (\Here => Refl)
 
 export
-assoc :
-  (thin3 : sz `Thins` sw) ->
-  (thin2 : sy `Thins` sz) ->
-  (thin1 : sx `Thins` sy) ->
-  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
-assoc Empty thin2 thin1 = Refl
-assoc (Drop thin3) thin2 thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Drop thin2) thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Keep thin2) (Drop thin1) = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Keep thin2) (Keep thin1) = cong Keep (assoc thin3 thin2 thin1)
+keepEmptyIsPoint : Keep Empty <~> Point Here
+keepEmptyIsPoint = MkEquivalence (\Here => Refl)
 
+-- Operations ------------------------------------------------------------------
+
+||| Composition of two thinnings.
 export
-indexId : (len : Len sx) => (i : Elem x sx) -> index (id @{len}) i = i
-indexId {len = S k} Here = Refl
-indexId {len = S k} (There i) = cong There (indexId i)
+(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
+Id . thin1 = thin1
+Empty . Id = Empty
+Empty . Empty = Empty
+Drop thin2 . Id = Drop thin2
+Drop thin2 . Empty = Empty
+Drop thin2 . Drop thin1 = Drop (thin2 . Drop thin1)
+Drop thin2 . Keep thin1 = Drop (thin2 . Keep thin1)
+Keep thin2 . Id = Keep thin2
+Keep thin2 . Empty = Empty
+Keep thin2 . Drop thin1 = Drop (thin2 . thin1)
+Keep thin2 . Keep thin1 = Keep (thin2 . thin1)
+
+--- Properties
 
 export
 indexHomo :
@@ -248,69 +189,224 @@ indexHomo :
   (thin1 : sx `Thins` sy) ->
   (i : Elem x sx) ->
   index thin2 (index thin1 i) = index (thin2 . thin1) i
+indexHomo Id thin1 i = Refl
+indexHomo Empty Id i impossible
 indexHomo Empty Empty i impossible
-indexHomo (Drop thin2) thin1 i = cong There (indexHomo thin2 thin1 i)
-indexHomo (Keep thin2) (Drop thin1) i = cong There (indexHomo thin2 thin1 i)
+indexHomo (Drop thin2) Id i = Refl
+indexHomo (Drop thin2) (Drop thin1) i = cong There $ indexHomo thin2 (Drop thin1) i
+indexHomo (Drop thin2) (Keep thin1) i = cong There $ indexHomo thin2 (Keep thin1) i
+indexHomo (Keep thin2) Id i = Refl
+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)
+indexHomo (Keep thin2) (Keep thin1) (There i) = cong There $ indexHomo thin2 thin1 i
 
--- Objects
+-- Categorical
 
 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)
+identityLeft : (thin : sx `Thins` sy) -> Id . thin <~> thin
+identityLeft thin = reflexive
 
 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)
+identityRight : (thin : sx `Thins` sy) -> thin . Id <~> thin
+identityRight Id = reflexive
+identityRight Empty = reflexive
+identityRight (Drop thin) = reflexive
+identityRight (Keep thin) = reflexive
 
 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)
+assoc :
+  (thin3 : sz `Thins` sw) ->
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  thin3 . (thin2 . thin1) <~> (thin3 . thin2) . thin1
+assoc thin3 thin2 thin1 = MkEquivalence (\i => Calc $
+  |~ index (thin3 . (thin2 . thin1)) i
+  ~~ index thin3 (index (thin2 . thin1) i)     ..<(indexHomo thin3 (thin2 . thin1) i)
+  ~~ index thin3 (index thin2 (index thin1 i)) ..<(cong (index thin3) $ indexHomo thin2 thin1 i)
+  ~~ index (thin3 . thin2) (index thin1 i)     ...(indexHomo thin3 thin2 (index thin1 i))
+  ~~ index ((thin3 . thin2) . thin1) i         ...(indexHomo (thin3 . thin2) thin1) i)
 
-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
+-- Other
 
 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
+dropLeft :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  Drop thin2 . thin1 <~> Drop (thin2 . thin1)
+dropLeft thin2 Id = symmetric $ dropCong $ identityRight thin2
+dropLeft thin2 Empty = emptyUnique Empty (Drop (thin2 . Empty))
+dropLeft thin2 (Drop thin1) = reflexive
+dropLeft thin2 (Keep thin1) = reflexive
 
 export
-wknId : (len : Len sx) => (v : Thinned t sx) -> wkn v (id @{len}) = v
-wknId (value `Over` thin) = cong (value `Over`) $ identityLeft thin
+keepDrop :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  Keep thin2 . Drop thin1 <~> Drop (thin2 . thin1)
+keepDrop thin2 thin1 = reflexive
 
 export
-wknHomo :
-  (v : Thinned t sx) ->
+keepHomo :
   (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
+  Keep thin2 . Keep thin1 <~> Keep (thin2 . thin1)
+keepHomo thin2 thin1 = reflexive
+
+export
+pointRight :
+  (thin : sx `Thins` sy) ->
+  (i : Elem x sx) ->
+  thin . Point i <~> Point (index thin i)
+pointRight Id i = reflexive
+pointRight (Drop thin) i = transitive (dropLeft thin (Point i)) (dropCong (pointRight thin i))
+pointRight (Keep thin) Here = keepCong (emptyUnique (thin . Empty) Empty)
+pointRight (Keep thin) (There i) = dropCong (pointRight thin i)
+
+-- Coverings and Coproducts ----------------------------------------------------
 
-%hint
+||| Proof that the thinnings are jointly surjective.
+public export
+record Covering (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where
+  constructor MkCovering
+  covers :
+    forall x.
+    (i : Elem x sz) ->
+    Either (j ** index thin1 j = i) (k ** index thin2 k = i)
+
+||| Unique thinning that factors into a covering.
+public export
+record Coproduct (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where
+  constructor MkCoproduct
+  {0 sw : SnocList _}
+  {thin1' : sx `Thins` sw}
+  {thin2' : sy `Thins` sw}
+  {factor : sw `Thins` sz}
+  0 left : factor . thin1' <~> thin1
+  0 right : factor . thin2' <~> thin2
+  0 cover : Covering thin1' thin2'
+
+%name Covering cover
+%name Coproduct cp
+
+--- Properties
+
+-- Coverings
+
+coverSym : Covering thin1 thin2 -> Covering thin2 thin1
+coverSym cover = MkCovering (\i => mirror $ cover.covers i)
+
+coverId : (0 thin : sx `Thins` sy) -> Covering Id thin
+coverId thin = MkCovering (\i => Left (i ** Refl))
+
+coverDropKeep : Covering thin1 thin2 -> Covering (Drop thin1) (Keep thin2)
+coverDropKeep cover = MkCovering
+  (\i => case i of
+    Here => Right (Here ** Refl)
+    There i => case cover.covers i of
+      Left (j ** prf) => Left (j ** cong There prf)
+      Right (k ** prf) => Right (There k ** cong There prf))
+
+coverKeepDrop : Covering thin1 thin2 -> Covering (Keep thin1) (Drop thin2)
+coverKeepDrop cp = coverSym $ coverDropKeep $ coverSym cp
+
+coverKeepKeep : Covering thin1 thin2 -> Covering (Keep thin1) (Keep thin2)
+coverKeepKeep cover = MkCovering
+  (\i => case i of
+    Here => Left (Here ** Refl)
+    There i => case cover.covers i of
+      Left (j ** prf) => Left (There j ** cong There prf)
+      Right (k ** prf) => Right (There k ** cong There prf))
+
+-- Coproducts
+
+coprodSym : Coproduct thin1 thin2 -> Coproduct thin2 thin1
+coprodSym cp = MkCoproduct cp.right cp.left (coverSym cp.cover)
+
+coprodId : (thin : sx `Thins` sy) -> Coproduct Id thin
+coprodId thin =
+  MkCoproduct
+    { thin1' = Id
+    , thin2' = thin
+    , factor = Id
+    , left = reflexive
+    , right = reflexive
+    , cover = coverId thin
+    }
+
+coprodEmpty : (thin : sx `Thins` sy) -> Coproduct Empty thin
+coprodEmpty thin =
+  MkCoproduct
+    { thin1' = Empty
+    , thin2' = Id
+    , factor = thin
+    , left = emptyUnique (thin . Empty) Empty
+    , right = identityRight thin
+    , cover = coverSym $ coverId Empty
+    }
+
+||| Finds the coproduct of two thinnings.
 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
+coprod :
+  (thin1 : sx `Thins` sz) ->
+  (thin2 : sy `Thins` sz) ->
+  Coproduct thin1 thin2
+coprod Id thin2 = coprodId thin2
+coprod Empty thin2 = coprodEmpty thin2
+coprod (Drop thin1) Id = coprodSym $ coprodId (Drop thin1)
+coprod (Drop thin1) Empty = coprodSym $ coprodEmpty (Drop thin1)
+coprod (Drop thin1) (Drop thin2) =
+  let cp = coprod thin1 thin2 in
+  MkCoproduct
+    { thin1' = cp.thin1'
+    , thin2' = cp.thin2'
+    , factor = Drop cp.factor
+    , left = transitive (dropLeft cp.factor cp.thin1') (dropCong cp.left)
+    , right = transitive (dropLeft cp.factor cp.thin2') (dropCong cp.right)
+    , cover = cp.cover
+    }
+coprod (Drop thin1) (Keep thin2) =
+  let cp = coprod thin1 thin2 in
+  MkCoproduct
+    { thin1' = Drop cp.thin1'
+    , thin2' = Keep cp.thin2'
+    , factor = Keep cp.factor
+    , left = transitive (keepDrop cp.factor cp.thin1') (dropCong cp.left)
+    , right = transitive (keepHomo cp.factor cp.thin2') (keepCong cp.right)
+    , cover = coverDropKeep cp.cover
+    }
+coprod (Keep thin1) Id = coprodSym $ coprodId (Keep thin1)
+coprod (Keep thin1) Empty = coprodSym $ coprodEmpty (Keep thin1)
+coprod (Keep thin1) (Drop thin2) =
+  let cp = coprod thin1 thin2 in
+  MkCoproduct
+    { thin1' = Keep cp.thin1'
+    , thin2' = Drop cp.thin2'
+    , factor = Keep cp.factor
+    , left = transitive (keepHomo cp.factor cp.thin1') (keepCong cp.left)
+    , right = transitive (keepDrop cp.factor cp.thin2') (dropCong cp.right)
+    , cover = coverKeepDrop cp.cover
+    }
+coprod (Keep thin1) (Keep thin2) =
+  let cp = coprod thin1 thin2 in
+  MkCoproduct
+    { thin1' = Keep cp.thin1'
+    , thin2' = Keep cp.thin2'
+    , factor = Keep cp.factor
+    , left = transitive (keepHomo cp.factor cp.thin1') (keepCong cp.left)
+    , right = transitive (keepHomo cp.factor cp.thin2') (keepCong cp.right)
+    , cover = coverKeepKeep cp.cover
+    }
+
+-- Coproduct Equivalence -------------------------------------------------------
+
+namespace Coproduct
+  public export
+  data (<~>) :
+    {0 thin1 : sx `Thins` sa} ->
+    {0 thin2 : sy `Thins` sa} ->
+    {0 thin3 : sz `Thins` sa} ->
+    {0 thin4 : sw `Thins` sa} ->
+    Coproduct thin1 thin2 ->
+    Coproduct thin3 thin4 ->
+    Type
+    where
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)
diff --git a/src/Type.idr b/src/Type.idr
new file mode 100644
index 0000000..12c0a74
--- /dev/null
+++ b/src/Type.idr
@@ -0,0 +1,10 @@
+module Type
+
+infix 4 ~>
+
+public export
+data Ty : Type where
+  N : Ty
+  (~>) : Ty -> Ty -> Ty
+
+%name Ty ty