diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 2a272bf..b2b3daf 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -474,7 +474,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
           compare0 ctx (sub1 eret (Zero :# Nat)) ezer fzer
           let [< p, ih] = esuc.names
           compare0 (extendTyN [< (epi, p, Nat), (epi', ih, eret.term)] ctx)
-                   (weakT eret.term)
+                   (substCaseSuccRet eret)
                    esuc.term fsuc.term
           expectEqualQ epi  fpi
           expectEqualQ epi' fpi'
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 7c6b6b7..76aa585 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -384,7 +384,7 @@ parameters {auto _ : IsQty q}
     let [< p, ih] = suc.names
         pisg      = pi * sg.fst
         sucCtx    = extendTyN [< (pisg, p, Nat), (pi', ih, ret.term)] ctx
-        sucType   = substCaseNatRet ret
+        sucType   = substCaseSuccRet ret
     sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
     let Just armout = lubs ctx [zerout, sucout]
           | _ => throw $ BadCaseQtys ctx $
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 9da8d50..1ae82c7 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -44,12 +44,12 @@ lookupFree' defs x =
 public export
 substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
 substCasePairRet dty retty =
-  let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
+  let arg = Pair (BVT 1) (BVT 0) :# (dty // fromNat 2) in
   retty.term // (arg ::: shift 2)
 
 public export
-substCaseNatRet : ScopeTerm q d n -> Term q d (2 + n)
-substCaseNatRet retty = retty.term // (Succ (BVT 1) :# Nat ::: shift 2)
+substCaseSuccRet : ScopeTerm q d n -> Term q d (2 + n)
+substCaseSuccRet retty = retty.term // (Succ (BVT 1) :# Nat ::: shift 2)
 
 public export
 substCaseBoxRet : Term q d n -> ScopeTerm q d n -> Term q d (S n)