1 files changed, 8 insertions, 9 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index ae7e3aa..2fff434 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -27,9 +27,9 @@ data EnvWf where
     EnvWf [<]
   (:<) :
     EnvWf env ->
-    TypeWf env (wkn a thin) ->
+    TypeWf env (expand t) ->
     ---
-    EnvWf (Add env thin a)
+    EnvWf (Add env t)
 
 data TypeWf where
   SetType :
@@ -150,11 +150,10 @@ data TermConv where
 public export
 data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where
   IdWf : ThinWf (id sx) env env
-  DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 thin' a) env1
+  DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 t) env1
   KeepWf :
     ThinWf thin env2 env1 ->
-    {auto 0 prf : IsNotId thin} ->
-    ThinWf (keep thin n) (Add env2 (thin . thin') a) (Add env1 thin' a)
+    ThinWf (keep thin n) (Add env2 (shift t thin)) (Add env1 t)
 
 %name ThinWf thinWf
 
@@ -166,7 +165,7 @@ typeConvRespEnvEq : TypeConv env1 a b -> EnvEq env1 env2 -> TypeConv env2 a b
 termWfRespEnvEq : TermWf env1 t a -> EnvEq env1 env2 -> TermWf env2 t a
 termConvRespEnvEq : TermConv env1 t u b -> EnvEq env1 env2 -> TermConv env2 t u b
 
-envWfRespEnvEq [<] [<] = [<]
+envWfRespEnvEq envWf Base = envWf
 envWfRespEnvEq (envWf :< wf) (prf :< eq) =
   envWfRespEnvEq envWf prf :<
   rewrite sym eq in typeWfRespEnvEq wf prf
@@ -282,10 +281,10 @@ CompWf (KeepWf {thin = thin2, n} thinWf2) IdWf =
 CompWf (KeepWf {thin = thin2, n} thinWf2) (DropWf {thin = thin1} thinWf1) =
   rewrite compRightDrop thin2 thin1 n in
   DropWf (CompWf thinWf2 thinWf1)
-CompWf (KeepWf {thin = thin2, n, prf = prf2} thinWf2) (KeepWf {thin = thin1, thin', prf = prf1} thinWf1) =
+CompWf (KeepWf {thin = thin2, n} thinWf2) (KeepWf {thin = thin1, t} thinWf1) =
   rewrite compKeep thin2 thin1 n in
-  rewrite compAssoc thin2 thin1 thin' in
-  KeepWf {prf = compPresNotId prf2 prf1} (CompWf thinWf2 thinWf1)
+  rewrite shiftHomo t thin1 thin2 in
+  KeepWf (CompWf thinWf2 thinWf1)
 
 -- Weakening Preservation ------------------------------------------------------