diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr
index 1f299b9..4bb3727 100644
--- a/lib/Quox/Whnf/ComputeElimType.idr
+++ b/lib/Quox/Whnf/ComputeElimType.idr
@@ -11,24 +11,26 @@ import Quox.Displace
 ||| - assumes the elim is already typechecked
 ||| - the return value is not reduced
 export covering
-computeElimType : CanWhnf Term Interface.isRedexT =>
-                  CanWhnf Elim Interface.isRedexE =>
-                  {d, n : Nat} ->
-                  (defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
-                  (e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
-                  Eff Whnf (Term d n)
+computeElimType :
+  CanWhnf Term Interface.isRedexT =>
+  CanWhnf Elim Interface.isRedexE =>
+  {d, n : Nat} ->
+  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
+  Eff Whnf (Term d n)
 
 
 ||| computes a type and then reduces it to whnf
 export covering
-computeWhnfElimType0 : CanWhnf Term Interface.isRedexT =>
-                       CanWhnf Elim Interface.isRedexE =>
-                       {d, n : Nat} ->
-                       (defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
-                       (e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
-                       Eff Whnf (Term d n)
+computeWhnfElimType0 :
+  CanWhnf Term Interface.isRedexT =>
+  CanWhnf Elim Interface.isRedexE =>
+  {d, n : Nat} ->
+  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
+  Eff Whnf (Term d n)
 
-computeElimType defs ctx pi e {ne} =
+computeElimType defs ctx sg e =
   case e of
     F x u loc => do
       let Just def = lookup x defs
@@ -39,7 +41,7 @@ computeElimType defs ctx pi e {ne} =
       pure $ ctx.tctx !! i
 
     App f s loc =>
-      case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
         Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
         ty               => throw $ ExpectedPi loc ctx.names ty
 
@@ -47,12 +49,12 @@ computeElimType defs ctx pi e {ne} =
       pure $ sub1 ret pair
 
     Fst pair loc =>
-      case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
         Sig {fst, _} => pure fst
         ty           => throw $ ExpectedSig loc ctx.names ty
 
     Snd pair loc =>
-      case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
         Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
         ty           => throw $ ExpectedSig loc ctx.names ty
 
@@ -66,7 +68,7 @@ computeElimType defs ctx pi e {ne} =
       pure $ sub1 ret box
 
     DApp {fun = f, arg = p, loc} =>
-      case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
         Eq {ty, _} => pure $ dsub1 ty p
         t          => throw $ ExpectedEq loc ctx.names t
 
@@ -82,5 +84,5 @@ computeElimType defs ctx pi e {ne} =
     TypeCase {ret, _} =>
       pure ret
 
-computeWhnfElimType0 defs ctx pi e =
-  computeElimType defs ctx pi e >>= whnf0 defs ctx pi
+computeWhnfElimType0 defs ctx sg e =
+  computeElimType defs ctx sg e >>= whnf0 defs ctx SZero