diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index b6c2686..c59f76f 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -75,13 +75,13 @@ C eqs     :<? d = C $ eqs :< d
 
 private %inline
 ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
-ifVar i p = map $ \q => if isYes $ q `decEq` B i then p else q
+ifVar i p = map $ \q => if q == B i then p else q
 
+-- (using decEq instead of (==) because of the proofs below)
 private %inline
 checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d
-checkConst Zero Zero eqs = C eqs
-checkConst One  One  eqs = C eqs
-checkConst _    _    _   = ZeroIsOne
+checkConst e f eqs = if isYes $ e `decEq` f then C eqs else ZeroIsOne
+
 
 export
 setConst : Var d -> DimConst -> DimEq' d -> DimEq d