Write an encoding for data types.

12 files changed, 691 insertions, 525 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index 8250352..519fa19 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -5,12 +5,10 @@ sourcedir = "src"
 options = "--total"
 
 modules
-  = Level0
-  , Level1
-  , NormalForm
-  , Term
-  , Thinning
+  = Thinning
+  , Total.Encoded.Util
   , Total.LogRel
   , Total.NormalForm
   , Total.Reduction
+  , Total.Syntax
   , Total.Term
diff --git a/src/Level0.idr b/src/Level0.idr
deleted file mode 100644
index bbe141f..0000000
--- a/src/Level0.idr
+++ /dev/null
@@ -1,123 +0,0 @@
-module Level0
-
-import Data.SnocList.Elem
-import NormalForm
-import Term
-import Thinning
-
-record Cont (a : Type) where
-  constructor Then
-  runCont : forall res. (a -> res) -> res
-
-Functor Cont where
-  map f (Then g) = Then (\k => k (g f))
-
-Applicative Cont where
-  pure x = Then (\k => k x)
-  Then f <*> Then v = Then (\k => f (\j => v (k . j)))
-
-Monad Cont where
-  join (Then f) = Then (\k => f (\c => runCont c k))
-
-data IsNormSubst : Subst ctx ctx' -> Type where
-  Base : IsNormSubst (Base thin)
-  (:<) : IsNormSubst sub -> IsNormal t -> IsNormSubst (sub :< t)
-
-%name IsNormSubst prf
-
-record NormSubst (ctx, ctx' : SnocList Ty) where
-  constructor MkNormSubst
-  forget : Subst ctx ctx'
-  0 isNormSubst : IsNormSubst forget
-
-%name NormSubst sub
-
-indexNormal : IsNormSubst sub -> (i : Elem ty ctx) -> IsNormal (index sub i)
-indexNormal Base i = Ntrl Var
-indexNormal (sub :< t) Here = t
-indexNormal (sub :< t) (There i) = indexNormal sub i
-
-index : NormSubst ctx' ctx -> Elem ty ctx -> Normal ctx' ty
-index sub i = MkNormal (index (forget sub) i) (indexNormal (isNormSubst sub) i)
-
-restrictNormal : IsNormSubst sub -> (thin : ctx3 `Thins` ctx2) -> IsNormSubst (restrict sub thin)
-restrictNormal Base thin = Base
-restrictNormal (sub :< t) Id = sub :< t
-restrictNormal (sub :< t) (Drop thin) = restrictNormal sub thin
-restrictNormal (sub :< t) (Keep thin) = restrictNormal sub thin :< t
-
-restrict : NormSubst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> NormSubst ctx1 ctx3
-restrict sub thin =
-  MkNormSubst
-    (restrict (forget sub) thin)
-    (restrictNormal (isNormSubst sub) thin)
-
-data Case : Type -> Type where
-  Eval :
-    Term ctx ty ->
-    NormSubst ctx' ctx ->
-    Case (Normal ctx' ty)
-  EvalSub :
-    Subst ctx' ctx ->
-    NormSubst ctx'' ctx' ->
-    Case (NormSubst ctx'' ctx)
-  App :
-    Normal ctx (ty ~> ty') ->
-    Normal ctx ty ->
-    Case (Normal ctx ty')
-  Rec :
-    Normal ctx N ->
-    Normal ctx ty ->
-    Normal (ctx :< ty) ty ->
-    Case (Normal ctx ty)
-
-partial
-eval : Case ret -> Cont (ret)
-eval (Eval (Var i) sub) = pure (index sub i)
-eval (Eval (Abs t) sub) = do
-  sub <- eval (EvalSub (forget sub) (MkNormSubst (Base $ Drop Id) Base))
-  let sub = MkNormSubst (forget sub :< Var Here) (isNormSubst sub :< Ntrl Var)
-  t <- eval (Eval t sub)
-  pure (MkNormal (Abs $ forget t) (Abs $ isNormal t))
-eval (Eval (App t u) sub) = do
-  t <- eval (Eval t sub)
-  u <- eval (Eval u sub)
-  eval (App t u)
-eval (Eval (Zero) sub) = pure (MkNormal Zero Zero)
-eval (Eval (Succ t) sub) = {forget $= Succ, isNormal $= Succ} <$> eval (Eval t sub)
-eval (Eval (Rec t u v) sub) = do
-  t <- eval (Eval t sub)
-  u <- eval (Eval u sub)
-  sub <- eval (EvalSub (forget sub) (MkNormSubst (Base $ Drop Id) Base))
-  let sub = MkNormSubst (forget sub :< Var Here) (isNormSubst sub :< Ntrl Var)
-  v <- eval (Eval v sub)
-  eval (Rec t u v)
-eval (Eval (Sub t sub') sub) = do
-  sub' <- eval (EvalSub sub' sub)
-  eval (Eval t sub')
-eval (EvalSub (Base thin) sub') = pure (restrict sub' thin)
-eval (EvalSub (sub :< t) sub') =
-  pure (\sub, t => MkNormSubst (forget sub :< forget t) (isNormSubst sub :< isNormal t)) <*>
-  eval (EvalSub sub sub') <*>
-  eval (Eval t sub')
-eval (App (MkNormal (Abs t) prf) u) =
-  eval (Eval t (MkNormSubst (Base Id :< forget u) (Base :< isNormal u)))
-eval (App (MkNormal t@(Var _) prf) u) =
-  pure (MkNormal (App t (forget u)) (Ntrl $ App Var (isNormal u)))
-eval (App (MkNormal t@(App _ _) prf) u) =
-  pure (MkNormal (App t (forget u)) (Ntrl $ App (appNtrl prf) (isNormal u)))
-eval (App (MkNormal t@(Rec _ _ _) prf) u) =
-  pure (MkNormal (App t (forget u)) (Ntrl $ App (recNtrl prf) (isNormal u)))
-eval (Rec (MkNormal Zero prf) u v) = pure u
-eval (Rec (MkNormal (Succ t) prf) u v) = do
-  val <- eval (Rec (MkNormal t (predNorm prf)) u v)
-  eval (Eval (forget v) (MkNormSubst (Base Id :< forget val) (Base :< isNormal val)))
-eval (Rec (MkNormal t@(Var _) prf) u v) =
-  pure $
-  MkNormal (Rec t (forget u) (forget v)) (Ntrl $ Rec Var (isNormal u) (isNormal v))
-eval (Rec (MkNormal t@(App _ _) prf) u v) =
-  pure $
-  MkNormal (Rec t (forget u) (forget v)) (Ntrl $ Rec (appNtrl prf) (isNormal u) (isNormal v))
-eval (Rec (MkNormal t@(Rec _ _ _) prf) u v) =
-  pure $
-  MkNormal (Rec t (forget u) (forget v)) (Ntrl $ Rec (recNtrl prf) (isNormal u) (isNormal v))
diff --git a/src/Level1.idr b/src/Level1.idr
deleted file mode 100644
index d269eb6..0000000
--- a/src/Level1.idr
+++ /dev/null
@@ -1,247 +0,0 @@
-module Level1
-
-import Data.DPair
-import Data.SnocList.Elem
-import NormalForm
-import Term
-import Thinning
-
-%hide NormalForm.Normal
-
-data IsNormSubst : Subst ctx ctx' -> Type where
-  Base : IsNormSubst (Base thin)
-  (:<) : IsNormSubst sub -> IsNormal t -> IsNormSubst (sub :< t)
-
-%name IsNormSubst prf
-
-Normal : SnocList Ty -> Ty -> Type
-Normal ctx ty = Subset (Term ctx ty) IsNormal
-
-NormSubst : SnocList Ty -> SnocList Ty -> Type
-NormSubst ctx ctx' = Subset (Subst ctx ctx') IsNormSubst
-
-indexNormal : IsNormSubst sub -> (i : Elem ty ctx) -> IsNormal (index sub i)
-indexNormal Base i = Ntrl Var
-indexNormal (sub :< t) Here = t
-indexNormal (sub :< t) (There i) = indexNormal sub i
-
-index : NormSubst ctx' ctx -> Elem ty ctx -> Normal ctx' ty
-index sub i = Element (index (fst sub) i) (indexNormal (snd sub) i)
-
-restrictNormal : IsNormSubst sub -> (thin : ctx3 `Thins` ctx2) -> IsNormSubst (restrict sub thin)
-restrictNormal Base thin = Base
-restrictNormal (sub :< t) Id = sub :< t
-restrictNormal (sub :< t) (Drop thin) = restrictNormal sub thin
-restrictNormal (sub :< t) (Keep thin) = restrictNormal sub thin :< t
-
-restrict : NormSubst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> NormSubst ctx1 ctx3
-restrict sub thin = Element (restrict (fst sub) thin) (restrictNormal (snd sub) thin)
-
-data Value : Type where
-  V : (ctx : SnocList Ty) -> (ty : Ty) -> Value
-  S : (ctx, ctx' : SnocList Ty) -> Value
-
-Raw : Value -> Type
-Raw (V ctx ty) = Term ctx ty
-Raw (S ctx ctx') = Subst ctx ctx'
-
-Norm : (a : Value) -> Raw a -> Type
-Norm (V _ _) = IsNormal
-Norm (S _ _) = IsNormSubst
-
-data Cont : Value -> Value -> Type where
-  EvalAbs1 : Term (ctx :< ty) ty' -> Cont (S (ctx' :< ty) ctx) (V ctx' (ty ~> ty'))
-  EvalAbs2 : Cont (V (ctx :< ty) ty') (V ctx (ty ~> ty'))
-  EvalApp1 : Term ctx ty -> NormSubst ctx' ctx -> Cont (V ctx' (ty ~> ty')) (V ctx' ty')
-  EvalApp2 : Normal ctx (ty ~> ty') -> Cont (V ctx ty) (V ctx ty')
-  EvalSucc1 : Cont (V ctx N) (V ctx N)
-  EvalRec1 :
-    Term ctx ty ->
-    Term (ctx :< ty) ty ->
-    NormSubst ctx' ctx ->
-    Cont (V ctx' N) (V ctx' ty)
-  EvalRec2 :
-    Normal ctx' N ->
-    Term (ctx :< ty) ty ->
-    NormSubst ctx' ctx ->
-    Cont (V ctx' ty) (V ctx' ty)
-  EvalRec3 :
-    Normal ctx' N ->
-    Normal ctx' ty ->
-    Term (ctx :< ty) ty ->
-    Cont (S (ctx' :< ty) ctx) (V ctx' ty)
-  EvalRec4 :
-    Normal ctx N ->
-    Normal ctx ty ->
-    Cont (V (ctx :< ty) ty) (V ctx ty)
-  EvalSub1 : Term ctx ty -> Cont (S ctx' ctx) (V ctx' ty)
-  EvalSnoc1 :
-    Term ctx ty ->
-    NormSubst ctx' ctx ->
-    Cont (S ctx' ctx'') (S ctx' (ctx'' :< ty))
-  EvalSnoc2 : NormSubst ctx' ctx -> Cont (V ctx' ty) (S ctx' (ctx :< ty))
-  RecSucc1 : Normal (ctx :< ty) ty -> Cont (V ctx ty) (V ctx ty)
-
-data Stack : Value -> Value -> Type where
-  Nil : Stack a a
-  (::) : Cont a b -> Stack b c -> Stack a c
-
-%name Cont k
-%name Stack stack
-
-data Case : Value -> Type where
-  Eval : Term ctx ty -> NormSubst ctx' ctx -> Case (V ctx' ty)
-  EvalSub : Subst ctx' ctx -> NormSubst ctx'' ctx' -> Case (S ctx'' ctx)
-  App : Normal ctx (ty ~> ty') -> Normal ctx ty -> Case (V ctx ty')
-  Rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Case (V ctx ty)
-  Run : Subset (Raw a) (Norm a) -> Case a
-
-%name Case c
-
-%prefix_record_projections off
-
-record Config (ret : Value) where
-  constructor On
-  {0 a : Value}
-  c : Case a
-  stack : Stack a ret
-
-data NotDone : Config ret -> Type where
-  EvalNotDone : NotDone (Eval t sub `On` stack)
-  EvalSubNotDone : NotDone (EvalSub sub sub' `On` stack)
-  AppNotDone : NotDone (App t u `On` stack)
-  RecNotDone : NotDone (Rec t u v `On` stack)
-  RunSomeNotDone : NotDone (Run x `On` step :: stack)
-
-step : (config : Config ret) -> {auto 0 _ : NotDone config} -> Config ret
-step (Eval (Var i) sub `On` stack) =
-  Run (index sub i) `On`
-  stack
-step (Eval (Abs t) sub `On` stack) =
-  EvalSub (fst sub) (Element (Base $ Drop Id) Base) `On`
-  EvalAbs1 t :: stack
-step (Eval (App t u) sub `On` stack) =
-  Eval t sub `On`
-  EvalApp1 u sub :: stack
-step (Eval Zero sub `On` stack) =
-  Run (Element Zero Zero) `On`
-  stack
-step (Eval (Succ t) sub `On` stack) =
-  Eval t sub `On`
-  EvalSucc1 :: stack
-step (Eval (Rec t u v) sub `On` stack) =
-  Eval t sub `On`
-  EvalRec1 u v sub :: stack
-step (Eval (Sub t sub') sub `On` stack) =
-  EvalSub sub' sub `On`
-  EvalSub1 t :: stack
-step (EvalSub (Base thin) sub' `On` stack) =
-  Run (restrict sub' thin) `On`
-  stack
-step (EvalSub (sub :< t) sub' `On` stack) =
-  EvalSub sub sub' `On`
-  EvalSnoc1 t sub' :: stack
-step (App (Element (Abs t) prf) u `On` stack) =
-  Eval t (Element (Base Id :< fst u) (Base :< snd u)) `On`
-  stack
-step (App (Element t@(Var _) prf) u `On` stack) =
-  Run (Element (App t (fst u)) (Ntrl $ App Var (snd u))) `On`
-  stack
-step (App (Element t@(App _ _) prf) u `On` stack) =
-  Run (Element (App t (fst u)) (Ntrl $ App (appNtrl prf) (snd u))) `On`
-  stack
-step (App (Element t@(Rec _ _ _) prf) u `On` stack) =
-  Run (Element (App t (fst u)) (Ntrl $ App (recNtrl prf) (snd u))) `On`
-  stack
-step (App (Element t@(Sub _ _) prf) u `On` stack) = void $ absurd prf
-step (Rec (Element Zero prf) u v `On` stack) =
-  Run u `On`
-  stack
-step (Rec (Element (Succ t) prf) u v `On` stack) =
-  Rec (Element t (predNorm prf)) u v `On`
-  RecSucc1 v :: stack
-step (Rec (Element t@(Var _) prf) u v `On` stack) =
-  Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec Var (snd u) (snd v))) `On`
-  stack
-step (Rec (Element t@(App _ _) prf) u v `On` stack) =
-  Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec (appNtrl prf) (snd u) (snd v))) `On`
-  stack
-step (Rec (Element t@(Rec _ _ _) prf) u v `On` stack) =
-  Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec (recNtrl prf) (snd u) (snd v))) `On`
-  stack
-step (Rec (Element t@(Sub _ _) prf) u v `On` stack) = void $ absurd prf
-step (Run sub `On` EvalAbs1 t :: stack) =
-  Eval t (Element (fst sub :< Var Here) (snd sub :< Ntrl Var)) `On`
-  EvalAbs2 :: stack
-step (Run t `On` EvalAbs2 :: stack) =
-  Run (Element (Abs $ fst t) (Abs $ snd t)) `On`
-  stack
-step (Run t `On` EvalApp1 u sub :: stack) =
-  Eval u sub `On`
-  EvalApp2 t :: stack
-step (Run u `On` EvalApp2 t :: stack) =
-  App t u `On`
-  stack
-step (Run t `On` EvalSucc1 :: stack) =
-  Run (Element (Succ $ fst t) (Succ $ snd t)) `On`
-  stack
-step (Run t `On` EvalRec1 u v sub :: stack) =
-  Eval u sub `On`
-  EvalRec2 t v sub :: stack
-step (Run u `On` EvalRec2 t v sub :: stack) =
-  EvalSub (fst sub) (Element (Base $ Drop Id) Base) `On`
-  EvalRec3 t u v :: stack
-step (Run sub `On` EvalRec3 t u v :: stack) =
-  Eval v (Element (fst sub :< Var Here) (snd sub :< Ntrl Var)) `On`
-  EvalRec4 t u :: stack
-step (Run v `On` EvalRec4 t u :: stack) =
-  Rec t u v `On`
-  stack
-step (Run sub `On` EvalSub1 t :: stack) =
-  Eval t sub `On`
-  stack
-step (Run sub `On` EvalSnoc1 t sub' :: stack) =
-  Eval t sub' `On`
-  EvalSnoc2 sub :: stack
-step (Run t `On` EvalSnoc2 sub :: stack) =
-  Run (Element (fst sub :< fst t) (snd sub :< snd t)) `On`
-  stack
-step (Run val `On` RecSucc1 v :: stack) =
-  Eval (fst v) (Element (Base Id :< fst val) (Base :< snd val)) `On`
-  stack
-
-unwindStack : Raw a -> (stack : Stack a b) -> Raw b
-unwindStack x [] = x
-unwindStack sub (EvalAbs1 t :: stack) = unwindStack (Abs (Sub t (sub :< Var Here))) stack
-unwindStack t (EvalAbs2 :: stack) = unwindStack (Abs t) stack
-unwindStack t (EvalApp1 u sub :: stack) = unwindStack (App t (Sub u (fst sub))) stack
-unwindStack u (EvalApp2 t :: stack) = unwindStack (App (fst t) u) stack
-unwindStack t (EvalSucc1 :: stack) = unwindStack (Succ t) stack
-unwindStack t (EvalRec1 u v sub :: stack) =
-  unwindStack (Rec t (Sub u (fst sub)) (Sub v (Base (Drop Id) . fst sub :< Var Here))) stack
-unwindStack u (EvalRec2 t v sub :: stack) =
-  unwindStack (Rec (fst t) u (Sub v (Base (Drop Id) . fst sub :< Var Here))) stack
-unwindStack sub (EvalRec3 t u v :: stack) =
-  unwindStack (Rec (fst t) (fst u) (Sub v (sub :< Var Here))) stack
-unwindStack v (EvalRec4 t u :: stack) =
-  unwindStack (Rec (fst t) (fst u) v) stack
-unwindStack sub (EvalSub1 t :: stack) = unwindStack (Sub t sub) stack
-unwindStack sub (EvalSnoc1 t sub' :: stack) = unwindStack (sub :< Sub t (fst sub')) stack
-unwindStack t (EvalSnoc2 sub :: stack) = unwindStack (fst sub :< t) stack
-unwindStack val (RecSucc1 v :: stack) = unwindStack (Sub (fst v) (Base Id :< val)) stack
-
-unwind : Config a -> Raw a
-unwind (Eval t sub `On` stack) = unwindStack (Sub t $ fst sub) stack
-unwind (EvalSub sub sub' `On` stack) = unwindStack (fst sub' . sub) stack
-unwind (App t u `On` stack) = unwindStack (App (fst t) (fst u)) stack
-unwind (Rec t u v `On` stack) = unwindStack (Rec (fst t) (fst u) (fst v)) stack
-unwind (Run x `On` stack) = unwindStack (fst x) stack
-
-eval : Nat -> Config ret -> Raw ret
-eval 0 config = unwind config
-eval (S n) (Run x `On` []) = fst x
-eval (S n) config@(Run _ `On` _ :: _) = eval n (step config)
-eval (S n) config@(Eval _ _ `On` _) = eval n (step config)
-eval (S n) config@(EvalSub _ _ `On` _) = eval n (step config)
-eval (S n) config@(App _ _ `On` _) = eval n (step config)
-eval (S n) config@(Rec _ _ _ `On` _) = eval n (step config)
diff --git a/src/NormalForm.idr b/src/NormalForm.idr
deleted file mode 100644
index ea3b2c0..0000000
--- a/src/NormalForm.idr
+++ /dev/null
@@ -1,51 +0,0 @@
-module NormalForm
-
-import Data.SnocList.Elem
-import Term
-import Thinning
-
--- Neutrals and Normals --------------------------------------------------------
-
-public export
-data IsNeutral : Term ctx ty -> Type
-public export
-data IsNormal : Term ctx ty -> Type
-
-data IsNeutral where
-  Var : IsNeutral (Var i)
-  App : IsNeutral t -> IsNormal u -> IsNeutral (App t u)
-  Rec : IsNeutral t -> IsNormal u -> IsNormal v -> IsNeutral (Rec t u v)
-
-data IsNormal where
-  Ntrl : IsNeutral t -> IsNormal t
-  Abs : IsNormal t -> IsNormal (Abs t)
-  Zero : IsNormal Zero
-  Succ : IsNormal t -> IsNormal (Succ t)
-
-%name IsNeutral prf
-%name IsNormal prf
-
-public export
-record Normal (ctx : SnocList Ty) (ty : Ty) where
-  constructor MkNormal
-  forget : Term ctx ty
-  0 isNormal : IsNormal forget
-
-%name Normal n, m, k
-
--- Inversions ------------------------------------------------------------------
-
-export
-Uninhabited (IsNormal (Sub t sub)) where uninhabited (Ntrl prf) impossible
-
-export
-predNorm : IsNormal (Succ t) -> IsNormal t
-predNorm (Succ prf) = prf
-
-export
-appNtrl : IsNormal (App t u) -> IsNeutral (App t u)
-appNtrl (Ntrl prf) = prf
-
-export
-recNtrl : IsNormal (Rec t u v) -> IsNeutral (Rec t u v)
-recNtrl (Ntrl prf) = prf
diff --git a/src/Term.idr b/src/Term.idr
deleted file mode 100644
index fde8d9f..0000000
--- a/src/Term.idr
+++ /dev/null
@@ -1,87 +0,0 @@
-module Term
-
-import Data.SnocList.Elem
-import Thinning
-
-infixr 20 ~>
-
--- Types -----------------------------------------------------------------------
-
-public export
-data Ty : Type where
-  N : Ty
-  (~>) : Ty -> Ty -> Ty
-
-%name Ty ty
-
--- Terms -----------------------------------------------------------------------
-
-public export
-data Term : SnocList Ty -> Ty -> Type
-public export
-data Subst : SnocList Ty -> SnocList Ty -> Type
-
-data Term where
-  Var : (i : Elem ty ctx) -> Term ctx ty
-  Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty')
-  App : Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty'
-  Zero : Term ctx N
-  Succ : Term ctx N -> Term ctx N
-  Rec : Term ctx N -> Term ctx ty -> Term (ctx :< ty) ty -> Term ctx ty
-  Sub : Term ctx ty -> Subst ctx' ctx -> Term ctx' ty
-
-data Subst where
-  Base : ctx' `Thins` ctx -> Subst ctx ctx'
-  (:<) : Subst ctx ctx' -> Term ctx ty -> Subst ctx (ctx' :< ty)
-
-%name Term t, u, v
-%name Subst sub
-
-shift : Subst ctx ctx' -> Subst (ctx :< ty) ctx'
-shift (Base thin) = Base (Drop thin)
-shift (sub :< t) = shift sub :< Sub t (Base (Drop Id))
-
-export
-lift : Subst ctx ctx' -> Subst (ctx :< ty) (ctx' :< ty)
-lift (Base thin) = Base (keep thin)
-lift (sub :< t) = shift (sub :< t) :< Var Here
-
-public export
-index : Subst 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
-restrict : Subst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> Subst ctx1 ctx3
-restrict (Base thin') thin = Base (thin' . thin)
-restrict (sub :< t) Id = sub :< t
-restrict (sub :< t) (Drop thin) = restrict sub thin
-restrict (sub :< t) (Keep thin) = restrict sub thin :< t
-
-export
-(.) : Subst ctx1 ctx2 -> Subst ctx2 ctx3 -> Subst ctx1 ctx3
-sub2 . Base thin = restrict sub2 thin
-sub2 . (sub1 :< t) = sub2 . sub1 :< Sub t sub2
-
--- Equivalence -----------------------------------------------------------------
-
-public export
-data Equiv : Term ctx ty -> Term ctx ty -> Type where
-  Refl : Equiv t t
-  Sym : Equiv t u -> Equiv u t
-  Trans : Equiv t u -> Equiv u v -> Equiv t v
-  AbsCong : Equiv t u -> Equiv (Abs t) (Abs u)
-  AppCong : Equiv t1 t2 -> Equiv u1 u2 -> Equiv (App t1 u1) (App t2 u2)
-  SuccCong : Equiv t u -> Equiv (Succ t) (Succ u)
-  RecCong : Equiv t1 t2 -> Equiv u1 u2 -> Equiv v1 v2 -> Equiv (Rec t1 u1 v1) (Rec t2 u2 v2)
-  PiBeta : Equiv (App (Abs t) u) (Sub t (Base Id :< u))
-  NatBetaZ : Equiv (Rec Zero t u) t
-  NatBetaS : Equiv (Rec (Succ t) u v) (Sub v (Base Id :< Rec t u v))
-  SubVar : Equiv (Sub (Var i) sub) (index sub i)
-  SubAbs : Equiv (Sub (Abs t) sub) (Abs (Sub t $ lift sub))
-  SubApp : Equiv (Sub (App t u) sub) (App (Sub t sub) (Sub u sub))
-  SubZero : Equiv (Sub Zero sub) Zero
-  SubSucc : Equiv (Sub (Succ t) sub) (Succ (Sub t sub))
-  SubRec : Equiv (Sub (Rec t u v) sub) (Rec (Sub t sub) (Sub u sub) (Sub v $ lift sub))
-  SubSub : Equiv (Sub (Sub t sub1) sub2) (Sub t (sub2 . sub1))
diff --git a/src/Thinning.idr b/src/Thinning.idr
index a79f0f5..a9b724d 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -31,6 +31,11 @@ keep Id = Id
 keep (Drop thin) = Keep (Drop thin)
 keep (Keep thin) = Keep (Keep thin)
 
+public export
+empty : (sx : SnocList a) -> [<] `Thins` sx
+empty [<] = Id
+empty (sx :< x) = Drop (empty sx)
+
 -- Operations ------------------------------------------------------------------
 
 public export
diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr
new file mode 100644
index 0000000..705d74b
--- /dev/null
+++ b/src/Total/Encoded/Util.idr
@@ -0,0 +1,437 @@
+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 : Term ctx B
+  True = Zero
+
+  export
+  False : Term ctx B
+  False = Suc Zero
+
+  export
+  If : Term ctx B -> Term ctx ty -> Term ctx ty -> Term ctx ty
+  If t u v = Rec t u (Abs $ wkn v (Drop Id))
+
+namespace Arb
+  export
+  arb : {ty : Ty} -> Term [<] 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
+  injL : {t, u : Ty} -> Term [<] (t ~> (t <+> u))
+  export
+  injR : {t, u : Ty} -> Term [<] (u ~> (t <+> u))
+  export
+  prjL : {t, u : Ty} -> Term [<] ((t <+> u) ~> t)
+  export
+  prjR : {t, u : Ty} -> Term [<] ((t <+> u) ~> u)
+
+  injL {t = N, u = N} = Abs' (S Z) id
+  injL {t = N, u = u ~> u'} = Abs' (S $ S Z) (\n, _ => App (lift (prjR . injL)) n)
+  injL {t = t ~> t', u = N} = Abs' (S Z) id
+  injL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injL . f . lift prjL)
+
+  injR {t = N, u = N} = Abs' (S Z) id
+  injR {t = N, u = u ~> u'} = Abs' (S Z) id
+  injR {t = t ~> t', u = N} = Abs' (S $ S Z) (\n, _ => App (lift (prjL . injR)) n)
+  injR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injR . f . lift prjR)
+
+  prjL {t = N, u = N} = Abs' (S Z) id
+  prjL {t = N, u = u ~> u'} = Abs' (S Z) (\f => App (lift (prjL . injR) . f) (lift $ arb))
+  prjL {t = t ~> t', u = N} = Abs' (S Z) id
+  prjL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjL . f . lift injL)
+
+  prjR {t = N, u = N} = Abs' (S Z) id
+  prjR {t = N, u = u ~> u'} = Abs' (S Z) id
+  prjR {t = t ~> t', u = N} = Abs' (S Z) (\f => App (lift (prjR . injL) . f) (lift $ arb))
+  prjR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjR . f . lift injR)
+
+namespace Unit
+  export
+  Unit : Ty
+  Unit = N
+
+namespace Pair
+  export
+  (*) : Ty -> Ty -> Ty
+  t * u = B ~> (t <+> u)
+
+  export
+  pair : {t, u : Ty} -> Term [<] (t ~> u ~> (t * u))
+  pair = Abs' (S $ S $ S Z)
+    (\fst, snd, b => If b (App (lift injL) fst) (App (lift injR) snd))
+
+  export
+  fst : {t, u : Ty} -> Term [<] ((t * u) ~> t)
+  fst = Abs' (S Z) (\p => App (lift prjL . p) True)
+
+  export
+  snd : {t, u : Ty} -> Term [<] ((t * u) ~> u)
+  snd = Abs' (S Z) (\p => App (lift prjR . p) False)
+
+  export
+  mapSnd : {t, u, v : Ty} -> Term [<] ((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} -> Term [<] (tys ~>* Product tys)
+  pair' {tys = [<]} = arb
+  pair' {tys = tys :< ty} = Abs' (S $ S Z) (\p, t => App' (lift pair) [<p, t]) .* pair' {tys}
+
+  export
+  project : {tys : SnocList Ty} -> Elem ty tys -> Term [<] (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 : length tys = length tys'} ->
+    All (Term ctx) (zipWith (~>) tys tys') ->
+    Term ctx (Product tys ~> Product tys')
+  mapProd {tys = [<], tys' = [<]} [<] = Abs (Var Here)
+  mapProd {tys = tys :< ty, tys' = tys' :< ty', prf} (fs :< f) =
+    Abs' (S Z)
+      (\p =>
+        App' (lift pair)
+          [<App (wkn (mapProd fs {prf = injective prf}) (Drop Id) . lift fst) p
+          , App (wkn f (Drop Id) . 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} ->
+    Term [<] ((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} -> Term [<] (Vect 0 ty)
+  Nil = arb
+
+  export
+  Cons : {n : Nat} -> {ty : Ty} -> Term [<] (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} -> Term [<] (Vect (S n) ty ~> ty)
+  head = snd
+
+  export
+  tail : {n : Nat} -> {ty : Ty} -> Term [<] (Vect (S n) ty ~> Vect n ty)
+  tail = fst
+
+  export
+  index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> Term [<] (Vect n ty ~> ty)
+  index FZ = head
+  index (FS i) = index i . tail
+
+  export
+  enumerate : (n : Nat) -> Term [<] (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} -> Term [<] (t ~> (t + u))
+  left = Abs' (S Z) (\e => App' (lift pair) [<True, App (lift injL) e])
+
+  export
+  right : {t, u : Ty} -> Term [<] (u ~> (t + u))
+  right = Abs' (S Z) (\e => App' (lift pair) [<False, App (lift injR) e])
+
+  export
+  case' : {t, u, ty : Ty} -> Term [<] ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty)
+  case' = Abs' (S $ S $ S Z)
+    (\f, g, s =>
+      If (App (lift fst) s)
+        (App (f . lift (prjL . snd)) s)
+        (App (g . lift (prjR . snd)) s))
+
+  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)) ->
+    Term [<] (ty ~> Sum' ty' tys)
+  put' {tys = []} Here = Abs' (S Z) id
+  put' {tys = _ :: _} Here = left
+  put' {tys = _ :: _} (There i) = right . put' i
+
+  export
+  put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> Term [<] (ty ~> Sum tys)
+  put {tys = _ ::: _} i = put' i
+
+  caseAll' :
+    {ctx : SnocList Ty} ->
+    {ty, ty' : Ty} ->
+    {tys : List Ty} ->
+    All (Term ctx . (~> ty)) (ty' :: tys) ->
+    Term ctx (Sum' ty' tys ~> ty)
+  caseAll' (t :: []) = t
+  caseAll' (t :: u :: ts) = App' (lift case') [<t, caseAll' (u :: ts)]
+
+  export
+  caseAll :
+    {ctx : SnocList Ty} ->
+    {tys : List1 Ty} ->
+    {ty : Ty} ->
+    All (Term ctx . (~> ty)) (forget tys) ->
+    Term ctx (Sum tys ~> ty)
+  caseAll {tys = _ ::: _} = caseAll'
+
+namespace Nat
+  export
+  IsZero : Term [<] (N ~> B)
+  IsZero = Abs' (S Z) (\m => Rec m (lift True) (Abs (lift False)))
+
+  export
+  Add : Term [<] (N ~> N ~> N)
+  Add = Abs' (S $ S Z) (\m, n => Rec m n (Abs' (S Z) Suc))
+
+  export
+  sum : {n : Nat} -> Term [<] (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 : Term [<] (N ~> N)
+  Pred = Abs' (S Z)
+    (\m =>
+      App' (lift case')
+        [<Abs Zero
+        , Abs' (S Z) id
+        , Rec m
+            (lift $ App left (arb {ty = Unit}))
+            (App' (lift case')
+              [<Abs (lift $ App right Zero)
+              , Abs' (S Z) (\n => App (lift right) (Suc n))
+              ])
+        ])
+
+  export
+  Sub : Term [<] (N ~> N ~> N)
+  Sub = Abs' (S $ S Z) (\m, n => Rec n m (lift Pred))
+
+  export
+  LE : Term [<] (N ~> N ~> B)
+  LE = Abs' (S Z) (\m => lift IsZero . App (lift Sub) m)
+
+  export
+  LT : Term [<] (N ~> N ~> B)
+  LT = Abs' (S Z) (\m => App (lift LE) (Suc m))
+
+  export
+  Cond :
+    {ctx : SnocList Ty} ->
+    {ty : Ty} ->
+    List (Term ctx N, Term ctx (N ~> ty)) ->
+    Term ctx (N ~> ty)
+  Cond [] = lift arb
+  Cond ((n, v) :: xs) =
+    Abs' (S Z)
+      (\t =>
+        If (App' (lift LE) [<t, wkn n (Drop Id)])
+          (App (wkn v (Drop Id)) t)
+          (App (wkn (Cond xs) (Drop Id)) (App' (lift Sub) [<t, wkn n (Drop Id)])))
+
+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} ->
+    Term [<] ((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 : Term ctx (Vect n (fix c))) ->
+    (acc : Term ctx N) ->
+    List (Term ctx N, Term ctx (N ~> N))
+  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 : Term ctx (Vect n (fix c))) ->
+    (acc : Term ctx N) ->
+    List (Term ctx N, Term ctx (N ~> fill c N))
+  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) ->
+    Term [<] (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), wkn t (Drop Id)])))
+          :: calcData (App (lift snd) t) (Suc Zero)
+          )
+        ])
+
+  export
+  elim :
+    {c : Container} ->
+    {ctx : SnocList Ty} ->
+    {ty : Ty} ->
+    All (Term ctx . (~> ty) . flip Data.fillShape ty) (forget c) ->
+    Term ctx (fix c ~> ty)
+  elim cases = Abs' (S Z)
+    (\t =>
+      let tags = Suc (App (lift $ project $ There $ There Here) t) in
+      let offset = App (lift $ project $ There Here) (wkn t (Drop $ Drop Id)) in
+      let vals = App (lift $ project $ Here) (wkn t (Drop $ Drop Id)) in
+      App'
+        (Rec tags
+          (lift arb)
+          (Abs' (S $ S Z) (\rec, n =>
+            App
+              (caseAll {tys = map (flip fillShape N) c}
+                (rewrite forgetMap (flip fillShape N) c in
+                 gmap
+                   (\f =>
+                     wkn f (Drop $ Drop $ Drop Id) .
+                     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
index b0d60ea..1ed7276 100644
--- a/src/Total/LogRel.idr
+++ b/src/Total/LogRel.idr
@@ -6,6 +6,7 @@ import Total.Term
 
 %prefix_record_projections off
 
+public export
 LogRel :
   {ctx : SnocList Ty} ->
   (P : {ctx, ty : _} -> Term ctx ty -> Type) ->
@@ -21,6 +22,7 @@ LogRel p {ty = ty ~> ty'} t =
    LogRel p u ->
    LogRel p (App (wkn t thin) u))
 
+export
 escape :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
   {ty : Ty} ->
@@ -30,6 +32,7 @@ escape :
 escape {ty = N} pt = pt
 escape {ty = ty ~> ty'} (pt, app) = pt
 
+public export
 record PreserveHelper
   (P : {ctx, ty : _} -> Term ctx ty -> Type)
   (R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type) where
@@ -48,11 +51,22 @@ record PreserveHelper
     {ty : Ty} ->
     {0 t, u : Term ctx ty} ->
     P t ->
-    R t u ->
+    (0 _ : R t u) ->
     P u
 
 %name PreserveHelper help
 
+export
+backStepHelper :
+  {0 P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  (forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> (0 _ : u > t) -> P u) ->
+  PreserveHelper P (flip (>))
+backStepHelper pres =
+  MkPresHelper
+    (\thin, v, step => AppCong1 (wknStep step))
+    pres
+
+export
 preserve :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
   {R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type} ->
@@ -60,7 +74,7 @@ preserve :
   {0 t, u : Term ctx ty} ->
   PreserveHelper P R ->
   LogRel P t ->
-  R t u ->
+  (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 =
@@ -81,7 +95,7 @@ data AllLogRel : (P : {ctx, ty : _} -> Term ctx ty -> Type) -> Terms ctx' ctx ->
 
 index :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
-  (forall ty. (i : Elem ty ctx') -> LogRel P (Var i)) ->
+  ((i : Elem ty ctx') -> LogRel P (Var i)) ->
   {sub : Terms ctx' ctx} ->
   AllLogRel P sub ->
   (i : Elem ty ctx) ->
@@ -102,21 +116,24 @@ Valid p t =
   (allRel : AllLogRel p sub) ->
   LogRel p (subst t sub)
 
+public export
 record ValidHelper (P : {ctx, ty : _} -> Term ctx ty -> Type) where
   constructor MkValidHelper
-  var : forall ctx, ty. (i : Elem ty ctx) -> LogRel P (Var i)
-  abs : forall ctx, ty, ty'. {0 t : Term (ctx :< ty) ty'} -> LogRel P t -> P (Abs t)
+  var : forall ctx. {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (Var i)
+  abs : forall ctx, ty. {ty' : Ty} -> {0 t : Term (ctx :< ty) ty'} -> LogRel P t -> P (Abs t)
   zero : forall ctx. P {ctx} Zero
   suc : forall ctx. {0 t : Term ctx N} -> P t -> P (Suc t)
-  rec : forall ctx, ty.
+  rec :
+    {ctx : SnocList Ty} ->
+    {ty : Ty} ->
     {0 t : Term ctx N} ->
-    {0 u : Term ctx ty} ->
-    {0 v : Term ctx (ty ~> ty)} ->
+    {u : Term ctx ty} ->
+    {v : Term ctx (ty ~> ty)} ->
     LogRel P t ->
     LogRel P u ->
     LogRel P v ->
     LogRel P (Rec t u v)
-  step : forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> u > t -> P u
+  step : forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> (0 _ : u > t) -> P u
   wkn : forall ctx, ctx', ty.
     {0 t : Term ctx ty} ->
     P t ->
@@ -150,6 +167,7 @@ wknAllRel :
 wknAllRel help Base thin = Base
 wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin
 
+export
 allValid :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
   {ctx : SnocList Ty} ->
@@ -169,8 +187,6 @@ allValid help (Abs t) sub allRels =
       help.abs rec
   , \thin, u, rel =>
     let
-      helper : PreserveHelper P (flip (>))
-      helper = MkPresHelper (\thin, v, step => AppCong1 (wknStep step)) help.step
       eq :
         (subst (wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)) (Base Id :< u) =
          subst t (wknAll sub thin :< u))
@@ -190,7 +206,7 @@ allValid help (Abs t) sub allRels =
           ...(cong (subst t . (:< u)) $ baseComp thin sub)
     in
       preserve
-        helper
+        (backStepHelper help.step)
         (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel))
         (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)}
           eq
@@ -209,3 +225,13 @@ allValid help (Rec t u v) sub allRels =
   let relu = allValid help u sub allRels in
   let relv = allValid help v sub allRels in
   help.rec relt relu relv
+
+export
+allRel :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  ValidHelper P ->
+  (t : Term ctx ty) ->
+  P t
+allRel help t = rewrite sym $ substId t in escape (allValid help t (Base Id) Base)
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
index 93a1da7..b5580b5 100644
--- a/src/Total/NormalForm.idr
+++ b/src/Total/NormalForm.idr
@@ -1,5 +1,6 @@
 module Total.NormalForm
 
+import Total.LogRel
 import Total.Reduction
 import Total.Term
 
@@ -32,3 +33,113 @@ record NormalForm (0 t : Term ctx ty) where
   0 normal : Normal term
 
 %name NormalForm nf
+
+-- Strong Normalization Proof --------------------------------------------------
+
+invApp : Normal (App t u) -> Neutral (App t u)
+invApp (Ntrl n) = n
+
+invRec : Normal (Rec t u v) -> Neutral (Rec t u v)
+invRec (Ntrl n) = n
+
+invSuc : Normal (Suc t) -> Normal t
+invSuc (Suc n) = n
+
+wknNe : Neutral t -> Neutral (wkn t thin)
+wknNf : Normal t -> Normal (wkn t thin)
+
+wknNe Var = Var
+wknNe (App n m) = App (wknNe n) (wknNf m)
+wknNe (Rec n m k) = Rec (wknNe n) (wknNf m) (wknNf k)
+
+wknNf (Ntrl n) = Ntrl (wknNe n)
+wknNf (Abs n) = Abs (wknNf n)
+wknNf Zero = Zero
+wknNf (Suc n) = Suc (wknNf n)
+
+backStepsNf : NormalForm t -> (0 _ : u >= t) -> NormalForm u
+backStepsNf nf steps = MkNf nf.term (steps ++ nf.steps) nf.normal
+
+backStepsRel :
+  {ty : Ty} ->
+  {0 t, u : Term ctx ty} ->
+  LogRel (\t => NormalForm t) t ->
+  (0 _ : u >= t) ->
+  LogRel (\t => NormalForm t) u
+backStepsRel =
+  preserve {R = flip (>=)}
+    (MkPresHelper (\thin, v, steps => AppCong1' (wknSteps steps)) backStepsNf)
+
+ntrlRel : {ty : Ty} -> {t : Term ctx ty} -> (0 _ : Neutral t) -> LogRel (\t => NormalForm t) t
+ntrlRel {ty = N} n = MkNf t [<] (Ntrl n)
+ntrlRel {ty = ty ~> ty'} n =
+  ( MkNf t [<] (Ntrl n)
+  , \thin, u, rel =>
+    backStepsRel
+      (ntrlRel (App (wknNe n) (escape rel).normal))
+      (AppCong2' (escape rel).steps)
+  )
+
+recNf' :
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  {u : Term ctx ty} ->
+  {v : Term ctx (ty ~> ty)} ->
+  (t' : Term ctx N) ->
+  (0 n : Normal t') ->
+  LogRel (\t => NormalForm t) u ->
+  LogRel (\t => NormalForm t) v ->
+  LogRel (\t => NormalForm t) (Rec t' u v)
+recNf' Zero n relU relV = backStepsRel relU [<RecZero]
+recNf' (Suc t') n relU relV =
+  let rec = recNf' t' (invSuc n) relU relV in
+  let step : Rec (Suc t') u v > App (wkn v Id) (Rec t' u v) = rewrite wknId v in RecSuc in
+  backStepsRel (snd relV Id _ rec) [<step]
+recNf' t'@(Var _) n relU relV =
+  let nfU = escape relU in
+  let nfV = escape {ty = ty ~> ty} relV in
+  backStepsRel
+    (ntrlRel (Rec Var nfU.normal nfV.normal))
+    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
+recNf' t'@(App _ _) n relU relV =
+  let nfU = escape relU in
+  let nfV = escape {ty = ty ~> ty} relV in
+  backStepsRel
+    (ntrlRel (Rec (invApp n) nfU.normal nfV.normal))
+    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
+recNf' t'@(Rec _ _ _) n relU relV =
+  let nfU = escape relU in
+  let nfV = escape {ty = ty ~> ty} relV in
+  backStepsRel
+    (ntrlRel (Rec (invRec n) nfU.normal nfV.normal))
+    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
+
+recNf :
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  {0 t : Term ctx N} ->
+  {u : Term ctx ty} ->
+  {v : Term ctx (ty ~> ty)} ->
+  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)
+    (RecCong1' nf.steps)
+
+helper : ValidHelper (\t => NormalForm t)
+helper = MkValidHelper
+  { var = \i => ntrlRel Var
+  , abs = \rel => let nf = escape rel in MkNf (Abs nf.term) (AbsCong' nf.steps) (Abs nf.normal)
+  , zero = MkNf Zero [<] Zero
+  , suc = \nf => MkNf (Suc nf.term) (SucCong' nf.steps) (Suc nf.normal)
+  , rec = recNf
+  , step = \nf, step => backStepsNf nf [<step]
+  , wkn = \nf, thin => MkNf (wkn nf.term thin) (wknSteps nf.steps) (wknNf nf.normal)
+  }
+
+export
+normalize : {ctx : SnocList Ty} -> {ty : Ty} -> (t : Term ctx ty) -> NormalForm t
+normalize = allRel helper
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index 4870f30..cb13706 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -95,3 +95,8 @@ 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
new file mode 100644
index 0000000..6a61cf5
--- /dev/null
+++ b/src/Total/Syntax.idr
@@ -0,0 +1,83 @@
+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
+
+infixr 20 ~>*
+infix 9 .*
+
+public export
+(~>*) : SnocList Ty -> Ty -> Ty
+tys ~>* ty = foldr (~>) ty tys
+
+public export
+data Len : SnocList Ty -> Type where
+  Z : Len [<]
+  S : Len tys -> Len (tys :< ty)
+
+%name Len k, m, n
+
+public export
+0 Fun : Len tys -> (Ty -> Type) -> Type -> Type
+Fun Z arg ret = ret
+Fun (S {ty} k) arg ret = Fun k arg (arg ty -> ret)
+
+after : (k : Len tys) -> (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 tys) ->
+  (forall ty. p ty -> q ty) ->
+  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 : Nat -> Term ctx N
+Lit 0 = Zero
+Lit (S n) = Suc (Lit n)
+
+AbsHelper :
+  (k : Len tys) ->
+  Fun k (flip Elem (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
+  Term ctx (tys ~>* ty)
+AbsHelper Z x = x
+AbsHelper (S k) x =
+  AbsHelper k $
+  after k (\f => Term.Abs (f SnocList.Elem.Here)) $
+  before k SnocList.Elem.There x
+
+export
+Abs' :
+  (k : Len tys) ->
+  Fun k (Term (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
+  Term ctx (tys ~>* ty)
+Abs' k = AbsHelper k . before k Var
+
+export
+App' : {tys : SnocList Ty} -> Term ctx (tys ~>* ty) -> All (Term ctx) tys -> Term ctx ty
+App' t [<] = t
+App' t (us :< u) = App (App' t us) u
+
+export
+(.) : {ty, ty' : Ty} -> Term ctx (ty' ~> ty'') -> Term ctx (ty ~> ty') -> Term ctx (ty ~> ty'')
+t . u = Abs' (S Z) (\x => App (wkn t (Drop Id)) (App (wkn u (Drop Id)) x))
+
+export
+(.*) :
+  {ty : Ty} ->
+  {tys : SnocList Ty} ->
+  Term ctx (ty ~> ty') ->
+  Term ctx (tys ~>* ty) ->
+  Term ctx (tys ~>* ty')
+(.*) {tys = [<]} t u = App t u
+(.*) {tys = tys :< ty''} t u = Abs' (S Z) (\f => wkn t (Drop Id) . f) .*  u
+
+export
+lift : {ctx : SnocList Ty} -> Term [<] ty -> Term ctx ty
+lift t = wkn t (empty ctx)
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 1530981..d4da92a 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -322,6 +322,15 @@ baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
 -- Substitution
 
 export
+substId : (t : Term ctx ty) -> subst t (Base Id) = t
+substId (Var i) = Refl
+substId (Abs t) = 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) ->