diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 9fe713e..67d5100 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -499,16 +499,18 @@ parameters (defs : Definitions)
 
       --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
       --  Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
-      --  Ψ | Γ ⊢ e <: f ⇒ _
-      --    (non-neutral forms have the coercion already pushed in)
+      --  Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
       -- -----------------------------------------------------------
-      --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e
-      --       <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ B‹q₂/𝑖›
-      compare0' ctx (Coe ty1 p1 q1 (E val1) _)
-                    (Coe ty2 p2 q2 (E val2) _) ne nf = do
-        compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
-        compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
-        compare0 ctx val1 val2
+      --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
+      --       <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
+      compare0' ctx (Coe ty1 p1 q1 val1 _)
+                    (Coe ty2 p2 q2 val2 _) ne nf = do
+        let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
+            ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
+        compareType ctx ty1p ty2p
+        compareType ctx ty1q ty2q
+        let ty_p = case !mode of Super => ty1p; _ => ty2p
+        Term.compare0 ctx ty_p val1 val2
       compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
 
       -- (no neutral compositions in a closed dctx)