diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 3ec9c0a..470fd2b 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -259,15 +259,16 @@ namespace Term
           compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
         SOne => clashT loc ctx ty s t
 
-  compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Enum cases _) s t = local_ Equal $
+    -- η for empty & singleton enums
+    if length (SortedSet.toList cases) <= 1 then pure () else
     case (s, t) of
       -- --------------------
-      --  Γ ⊢ `t = `t ⇐ {ts}
+      --  Γ ⊢ 't = 't ⇐ {ts}
       --
       -- t ∈ ts is in the typechecker, not here, ofc
-      (Tag t1 {}, Tag t2 {}) =>
-        unless (t1 == t2) $ clashT s.loc ctx ty s t
-      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
+      (Tag t1 {}, Tag t2 {}) => unless (t1 == t2) $ clashT s.loc ctx ty s t
+      (E e,       E f)       => ignore $ Elim.compare0 defs ctx sg e f
 
       (Tag {}, E _)    => clashT s.loc ctx ty s t
       (E _,    Tag {}) => clashT s.loc ctx ty s t