diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 1d272c3..2d9c493 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -235,10 +235,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     (tfst, tsnd) <- expectSig !ask pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
-    -- with ρ₁, ρ₂ ≤ π
+    -- with ρ₁, ρ₂ ≤ πσ
     let bodyctx = extendTyN [< tfst, tsnd.term] ctx
         bodyty  = substCasePairRet pairres.type ret
-    bodyout <- popQs [< pi, pi] !(checkC bodyctx sg body.term bodyty)
+        pisg    = pi * sg.fst
+    bodyout <- popQs [< pisg, pisg] !(checkC bodyctx sg body.term bodyty)
     -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret pair,