Give a logical relation template.

6 files changed, 540 insertions, 1 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index 21fe018..8250352 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -10,6 +10,7 @@ modules
   , NormalForm
   , Term
   , Thinning
+  , Total.LogRel
   , Total.NormalForm
   , Total.Reduction
   , Total.Term
diff --git a/src/Thinning.idr b/src/Thinning.idr
index 0e99711..a79f0f5 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -142,3 +142,12 @@ keepHomo (Drop thin2) (Keep thin1) = Refl
 keepHomo (Keep thin2) Id = Refl
 keepHomo (Keep thin2) (Drop thin) = Refl
 keepHomo (Keep thin2) (Keep thin) = Refl
+
+export
+keepDrop :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  keep thin2 . Drop thin1 = Drop (thin2 . thin1)
+keepDrop Id thin1 = Refl
+keepDrop (Drop thin2) thin1 = Refl
+keepDrop (Keep thin2) thin1 = Refl
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr
new file mode 100644
index 0000000..b0d60ea
--- /dev/null
+++ b/src/Total/LogRel.idr
@@ -0,0 +1,211 @@
+module Total.LogRel
+
+import Syntax.PreorderReasoning
+import Total.Reduction
+import Total.Term
+
+%prefix_record_projections off
+
+LogRel :
+  {ctx : SnocList Ty} ->
+  (P : {ctx, ty : _} -> Term ctx ty -> Type) ->
+  {ty : Ty} ->
+  (t : Term ctx ty) ->
+  Type
+LogRel p {ty = N} t = p t
+LogRel p {ty = ty ~> ty'} t =
+  (p t,
+   {ctx' : SnocList Ty} ->
+   (thin : ctx `Thins` ctx') ->
+   (u : Term ctx' ty) ->
+   LogRel p u ->
+   LogRel p (App (wkn t thin) u))
+
+escape :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {ty : Ty} ->
+  {0 t : Term ctx ty} ->
+  LogRel P t ->
+  P t
+escape {ty = N} pt = pt
+escape {ty = ty ~> ty'} (pt, app) = pt
+
+record PreserveHelper
+  (P : {ctx, ty : _} -> Term ctx ty -> Type)
+  (R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type) where
+  constructor MkPresHelper
+  app :
+    {0 ctx : SnocList Ty} ->
+    {ty, ty' : Ty} ->
+    {0 t, u : Term ctx (ty ~> ty')} ->
+    {ctx' : SnocList Ty} ->
+    (thin : ctx `Thins` ctx') ->
+    (v : Term ctx' ty) ->
+    R t u ->
+    R (App (wkn t thin) v) (App (wkn u thin) v)
+  pres :
+    {0 ctx : SnocList Ty} ->
+    {ty : Ty} ->
+    {0 t, u : Term ctx ty} ->
+    P t ->
+    R t u ->
+    P u
+
+%name PreserveHelper help
+
+preserve :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type} ->
+  {ty : Ty} ->
+  {0 t, u : Term ctx ty} ->
+  PreserveHelper P R ->
+  LogRel P t ->
+  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 : _} -> Term ctx ty -> Type) -> Terms ctx' ctx -> Type where
+  Base :
+    {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+    {0 thin : ctx `Thins` ctx'} ->
+    AllLogRel P (Base thin)
+  (:<) :
+    {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+    AllLogRel P sub ->
+    LogRel P t ->
+    AllLogRel P (sub :< t)
+
+%name AllLogRel allRels
+
+index :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  (forall ty. (i : Elem ty ctx') -> LogRel P (Var i)) ->
+  {sub : Terms ctx' ctx} ->
+  AllLogRel P sub ->
+  (i : Elem ty ctx) ->
+  LogRel P (index sub i)
+index f Base i = f (index _ i)
+index f (allRels :< rel) Here = rel
+index f (allRels :< rel) (There i) = index f allRels i
+
+Valid :
+  (P : {ctx, ty : _} -> Term ctx ty -> Type) ->
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  (t : Term ctx ty) ->
+  Type
+Valid p t =
+  {ctx' : SnocList Ty} ->
+  (sub : Terms ctx' ctx) ->
+  (allRel : AllLogRel p sub) ->
+  LogRel p (subst t sub)
+
+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)
+  zero : forall ctx. P {ctx} Zero
+  suc : forall ctx. {0 t : Term ctx N} -> P t -> P (Suc t)
+  rec : forall ctx, ty.
+    {0 t : Term ctx N} ->
+    {0 u : Term ctx ty} ->
+    {0 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
+  wkn : forall ctx, ctx', ty.
+    {0 t : Term ctx ty} ->
+    P t ->
+    (thin : ctx `Thins` ctx') ->
+    P (wkn t thin)
+
+%name ValidHelper help
+
+wknRel :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  ValidHelper P ->
+  {ty : Ty} ->
+  {0 t : Term ctx ty} ->
+  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 :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  ValidHelper P ->
+  {ctx : SnocList Ty} ->
+  {sub : Terms ctx' ctx} ->
+  AllLogRel P sub ->
+  (thin : ctx' `Thins` ctx'') ->
+  AllLogRel P (wknAll sub thin)
+wknAllRel help Base thin = Base
+wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin
+
+allValid :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  ValidHelper P ->
+  (t : Term ctx ty) ->
+  Valid P t
+allValid help (Var i) sub allRels = index help.var allRels i
+allValid help (Abs t) sub allRels =
+  let valid = allValid help t in
+  ( let
+      rec =
+        valid
+          (wknAll sub (Drop Id) :< Var Here)
+          (wknAllRel help allRels (Drop Id) :< help.var Here)
+    in
+      help.abs rec
+  , \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))
+      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))) $ restrictKeep (Base Id) u 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
+        helper
+        (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel))
+        (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)}
+          eq
+          AppBeta)
+  )
+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
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
index 7421ca9..93a1da7 100644
--- a/src/Total/NormalForm.idr
+++ b/src/Total/NormalForm.idr
@@ -3,6 +3,8 @@ module Total.NormalForm
 import Total.Reduction
 import Total.Term
 
+%prefix_record_projections off
+
 public export
 data Neutral : Term ctx ty -> Type
 public export
@@ -22,6 +24,7 @@ data Normal where
 %name Neutral n, m, k
 %name Normal n, m, k
 
+public export
 record NormalForm (0 t : Term ctx ty) where
   constructor MkNf
   term : Term ctx ty
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index efa6f74..4870f30 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -1,5 +1,6 @@
 module Total.Reduction
 
+import Syntax.PreorderReasoning
 import Total.Term
 
 public export
@@ -63,3 +64,34 @@ 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 Id :< wkn u thin) = wkn (subst t (Base 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 thin :< wkn u thin)
+    ...(cong (subst t) $ restrictKeep (Base Id) (wkn u thin) thin)
+  ~~ subst t (Base (thin . Id) :< wkn u thin)
+    ...(sym $ cong (subst t . (:< wkn u thin) . Base) $ identityRight thin)
+  ~~ wkn (subst t (Base Id :< u)) thin
+    ...(sym $ wknSubst t (Base Id :< 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 {t, u}) {thin} = rewrite sym $ lemma t thin u 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
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 22a9a39..1530981 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -2,6 +2,7 @@ module Total.Term
 
 import public Data.SnocList.Elem
 import public Thinning
+import Syntax.PreorderReasoning
 
 %prefix_record_projections off
 
@@ -25,6 +26,7 @@ data Term : SnocList Ty -> Ty -> Type where
 
 %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)
@@ -40,16 +42,18 @@ data Terms : SnocList Ty -> SnocList Ty -> Type where
 
 %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
 
-export
+public export
 subst : 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)
@@ -58,12 +62,291 @@ 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) Id = sub :< t
 restrict (sub :< t) (Drop thin) = restrict sub thin
 restrict (sub :< t) (Keep thin) = restrict sub thin :< t
 
+public export
 (.) : 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
+
+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 $ trans (wknHomo t (keep thin1) (keep thin2)) (cong (wkn t) $ keepHomo thin2 thin1)
+wknHomo (App t u) thin1 thin2 =
+  cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
+wknHomo Zero thin1 thin2 =
+  Refl
+wknHomo (Suc t) thin1 thin2 =
+  cong Suc (wknHomo t thin1 thin2)
+wknHomo (Rec t u v) thin1 thin2 =
+  cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2)
+
+export
+wknId : (t : Term ctx ty) -> wkn t Id = t
+wknId (Var i) = Refl
+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 Id (sub :< t) i = Refl
+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 : (sub : Terms ctx' ctx) -> restrict sub Id = sub
+restrictId (Base thin) = cong Base (identityRight thin)
+restrictId (sub :< t) = Refl
+
+export
+restrictKeep :
+  (sub : Terms ctx'' ctx) ->
+  (t : Term ctx'' ty) ->
+  (thin : ctx' `Thins` ctx) ->
+  restrict (sub :< t) (keep thin) = restrict sub thin :< t
+restrictKeep sub t Id = sym $ cong (:< t) $ restrictId sub
+restrictKeep sub t (Drop thin) = Refl
+restrictKeep sub t (Keep thin) = Refl
+
+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) Id thin2 = Refl
+restrictHomo (sub :< t) (Drop thin1) thin2 = restrictHomo sub thin1 thin2
+restrictHomo (sub :< t) (Keep thin1) Id = Refl
+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 Id (sub :< t) thin2 = Refl
+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)
+      ...(cong2 (\sub, i => subst t (sub :< Var i)) (wknAllHomo sub (Drop Id) (keep thin)) (indexKeepHere thin))
+    ~~ subst t (wknAll sub (Drop Id . thin) :< Var Here)
+      ...(cong (subst t . (:< Var Here) . wknAll sub) $ trans (keepDrop thin Id) (cong Drop $ identityRight 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) :< Var Here) (keep thin))
+      ...(substWkn t (keep thin) (wknAll sub (Drop Id) :< Var Here))
+    ~~ subst t (restrict (wknAll sub (Drop Id)) thin :< Var Here)
+      ...(cong (subst t) $ restrictKeep (wknAll sub (Drop Id)) (Var Here) thin)
+    ~~ 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 :
+      Equiv sub sub' ->
+      Equiv (wknAll sub (Drop Id) :< Var Here) (wknAll sub' (Drop Id) :< Var Here)
+
+  %name Equiv prf
+
+indexCong : Equiv sub sub' -> (i : Elem ty ctx) -> index sub i = index sub' i
+indexCong Base Here = irrelevantEq $ cong Var (indexKeepHere _)
+indexCong Base (There i) = irrelevantEq $ cong Var (indexKeepThere _ i)
+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 : (t : Term ctx ty) -> 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 = 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
+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)