diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 5998b3d..5ac02b2 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -278,13 +278,9 @@ namespace Term
 
     eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
     eta loc e (S _ (N b)) =
-      if qty /= One then
-        if !(isSubSing defs ctx sg arg) then
-          compare0 defs ctx' sg res.term (toLamBody e) (weakT 1 b)
-        else
-          clashT loc ctx ty s t
-      else
-        clashT loc ctx ty s t
+      if !(pure (qty /= One) `andM` isSubSing defs ctx sg arg)
+         then compare0 defs ctx' sg res.term (toLamBody e) (weakT 1 b)
+         else clashT loc ctx ty s t
     eta _ e (S _ (Y b)) =
       compare0 defs ctx' sg res.term (toLamBody e) b