diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index d4f9890..5efdcb3 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -347,9 +347,10 @@ parameters (defs : Definitions)
       --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
       compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
       compareType (extendDim sTy.name One  ctx) sTy.one  tTy.one
+      let ty = case !mode of Super => sTy; _ => tTy
       local_ Equal $ do
-        Term.compare0 ctx sTy.zero sl tl
-        Term.compare0 ctx sTy.one  sr tr
+        Term.compare0 ctx ty.zero sl tl
+        Term.compare0 ctx ty.one  sr tr
 
     compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
       -- ------------------