diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr
index d0d6033..702cafd 100644
--- a/lib/Quox/Syntax/Qty/Three.idr
+++ b/lib/Quox/Syntax/Qty/Three.idr
@@ -45,13 +45,11 @@ data Compat3 : Rel Three where
 
 public export
 compat3 : Dec2 Compat3
-compat3 pi rh with (decEq pi rh)
-  compat3 pi pi | Yes Refl = Yes CmpRefl
-  compat3 pi rh | No ne with (decEq rh Any)
-    compat3 pi Any | No ne | Yes Refl = Yes CmpAny
-    compat3 pi rh  | No ne | No  na   = No $ \case
-      CmpRefl => ne Refl
-      CmpAny  => na Refl
+compat3 pi rh with (decEq pi rh) | (decEq rh Any)
+  compat3 pi pi  | Yes Refl | _        = Yes CmpRefl
+  compat3 pi Any | No  _    | Yes Refl = Yes CmpAny
+  compat3 pi rh  | No  ne   | No  na   =
+    No $ \case CmpRefl => ne Refl; CmpAny => na Refl
 
 
 public export
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index 8cd4f84..0d901e6 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -240,10 +240,9 @@ eqReflect : (i, j : Var n) -> (i = j) `Reflects` (i == j)
 eqReflect VZ     VZ     = RTrue  Refl
 eqReflect VZ     (VS i) = RFalse absurd
 eqReflect (VS i) VZ     = RFalse absurd
-eqReflect (VS i) (VS j) with (eqReflect i j)
-  eqReflect (VS i) (VS j) | r with (i == j)
-    eqReflect (VS i) (VS j) | RTrue  yes | True   =  RTrue  $ cong VS yes
-    eqReflect (VS i) (VS j) | RFalse no  | False  =  RFalse $ no . injective
+eqReflect (VS i) (VS j) with (eqReflect i j) | (i == j)
+  _ | RTrue  yes | True  = RTrue  $ cong VS yes
+  _ | RFalse no  | False = RFalse $ no . injective
 
 public export
 reflectToDec : p `Reflects` b -> Dec p