diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index c97ed91..91d94d2 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -199,7 +199,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
             fstInSnd =
               CoeT !(fresh i)
                    (tfst // (BV 0 loc ::: shift 2))
-                   (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
+                   (weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
             snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
         whnf defs ctx sg $
           Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc