diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 470fd2b..83748af 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -236,8 +236,6 @@ namespace Term
       --  Γ ⊢ s₁ = t₁ ⇐ A     Γ ⊢ s₂ = t₂ ⇐ B{s₁/x}
       -- --------------------------------------------
       --     Γ ⊢ (s₁, t₁) = (s₂,t₂) ⇐ (x : A) × B
-      --
-      -- [todo] η for π ≥ 0 maybe
       (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
         compare0 defs ctx sg fst sFst tFst
         compare0 defs ctx sg (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
@@ -331,9 +329,9 @@ namespace Term
       --  Γ ⊢ [s] = [t] ⇐ [π.A]
       (Box s _, Box t _) => compare0 defs ctx sg ty s t
 
-      --   Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
-      -- -----------------------------------------------
-      --            Γ ⊢ [s] = e ⇐ [ρ.A]
+      --   Γ ⊢ σ⨴ρ · s = (case1 e return A of {[x] ⇒ x}) ⇐ A
+      -- -----------------------------------------------------
+      --               Γ ⊢ σ · [s] = e ⇐ [ρ.A]
       (Box s loc, E f)       => eta s f
       (E e,       Box t loc) => eta t e
 
@@ -347,7 +345,7 @@ namespace Term
     eta s e = do
       nm <- mnb "inner" e.loc
       let e = CaseBox One e (SN ty) (SY [< nm] (BVT 0 nm.loc)) e.loc
-      compare0 defs ctx sg ty s (E e)
+      compare0 defs ctx (sg `subjMult` q) ty s (E e)
 
   compare0' defs ctx sg ty@(E _) s t = do
     -- a neutral type can only be inhabited by neutral values