diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index f3faadd..3e6d8a4 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -97,8 +97,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
     -- ⇝
-    -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C
-    -- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
+    -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
     let ctx1 = extendDim i ctx
     Element ty tynf <- whnf defs ctx1 ty.term
     ta <- tycaseBOX defs ctx1 ty
@@ -110,9 +109,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   ||| pushes a coercion inside a whnf-ed term
   export covering
   pushCoe : BindName ->
-            (ty : Term (S d) n) ->
-            (p, q : Dim d) -> (0 npq : Not (p `Eqv` q)) =>
-            (s : Term d n) -> (0 pc : So (canPushCoe ty s)) => Loc ->
+            (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
+            (0 pc : So (canPushCoe ty s)) =>
             Eff Whnf (NonRedex Elim d n defs)
   pushCoe i ty p q s loc =
     case ty of