diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
--- a/examples/simple-arith.hs
+++ b/examples/simple-arith.hs
@@ -1,18 +1,17 @@
 {-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts, EmptyCase #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
-{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}
 module Main where
 import Data.Type.Equality
 import GHC.TypeLits       (Nat, type (<=), type (*), type (+), type (<=?), CmpNat)
 import Proof.Propositional (Empty(..))
 import Proof.Propositional (IsTrue(Witness))
-import Data.Singletons.Prelude
+import Data.Singletons.Prelude hiding (type (<=))
 import Data.Void
 
 type n <=! m = IsTrue (n <=? m)
 infix 4 <=!
 
-natLeqZero :: (n <= 0) => proxy n -> n :~: 0
+natLeqZero :: ((n <=? 0) ~ 'True) => proxy n -> n :~: 0
 natLeqZero _ = Refl
 
 -- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)
diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-presburger
-version:             0.2.0.1
+version:             0.2.0.2
 synopsis:            Presburger Arithmetic Solver for GHC Type-level natural numbers.
 description: 
   @ghc-typelits-presburger@ augments GHC type-system with Presburger Arithmetic Solver for Type-level natural numbers.
diff --git a/src/GHC/TypeLits/Presburger.hs b/src/GHC/TypeLits/Presburger.hs
--- a/src/GHC/TypeLits/Presburger.hs
+++ b/src/GHC/TypeLits/Presburger.hs
@@ -1,20 +1,17 @@
 {-# LANGUAGE FlexibleContexts, MultiWayIf, OverloadedStrings, PatternGuards #-}
-{-# LANGUAGE RankNTypes, TupleSections                                      #-}
+{-# LANGUAGE RankNTypes, RecordWildCards, TupleSections                     #-}
 module GHC.TypeLits.Presburger (plugin) where
 import GHC.Compat
 
 import           Class            (classTyCon)
 import           Data.Foldable    (asum)
-import           Data.Integer.SAT (Expr (..), Prop (..), PropSet)
-import           Data.Integer.SAT (assert, checkSat, noProps, toName)
+import           Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert)
+import           Data.Integer.SAT (checkSat, noProps, toName)
 import qualified Data.Integer.SAT as SAT
 import           Data.List        (nub)
-import           Data.Maybe       (catMaybes, fromMaybe, isNothing, mapMaybe)
-import           Data.Reflection  (Given)
-import           Data.Reflection  (given)
-import           Data.Reflection  (give)
-import           TcPluginM        (tcLookupClass)
-import           TcPluginM        (lookupOrig)
+import           Data.Maybe       (fromMaybe, isNothing, mapMaybe)
+import           Data.Reflection  (Given, give, given)
+import           TcPluginM        (lookupOrig, tcLookupClass)
 import           TysWiredIn       (promotedEQDataCon, promotedGTDataCon,
                                    promotedLTDataCon)
 
@@ -58,7 +55,7 @@
 
 presburgerPlugin :: TcPlugin
 presburgerPlugin =
-  tracePlugin "typelits-presburger" $
+  tracePlugin "typelits-presburger"
   TcPlugin { tcPluginInit  = return () -- tcPluginIO $ newIORef emptyTvSubst
            , tcPluginSolve = decidePresburger
            , tcPluginStop  = const $ return ()
@@ -69,13 +66,13 @@
 
 type PresState = ()
 
-data MyEnv  = MyEnv { emptyClsTyCon   :: TyCon
-                    , eqTyCon_        :: TyCon
-                    , eqWitCon_       :: TyCon
-                    , isTrueCon_      :: TyCon
-                    , voidTyCon       :: TyCon
-                    , singLeqCon_     :: TyCon
-                    , singCompareCon_ :: TyCon
+data MyEnv  = MyEnv { emptyClsTyCon     :: TyCon
+                    , eqTyCon_          :: TyCon
+                    , eqWitCon_         :: TyCon
+                    , isTrueCon_        :: TyCon
+                    , voidTyCon         :: TyCon
+                    , typeLeqBoolTyCon_ :: TyCon
+                    , singCompareCon_   :: TyCon
                     }
 
 eqTyCon :: Given MyEnv => TyCon
@@ -87,8 +84,8 @@
 isTrueTyCon :: Given MyEnv => TyCon
 isTrueTyCon = isTrueCon_ given
 
-singLeqCon :: Given MyEnv => TyCon
-singLeqCon = singLeqCon_ given
+typeLeqBoolTyCon :: Given MyEnv => TyCon
+typeLeqBoolTyCon = typeLeqBoolTyCon_ given
 
 singCompareCon :: Given MyEnv => TyCon
 singCompareCon = singCompareCon_ given
@@ -114,7 +111,7 @@
   tcPluginTrace "Env" $ ppr (emptyTyCon, eqTyCon, eqWitnessTyCon, isTrueTyCon)
   let subst = foldr (unionTvSubst . genSubst) emptyTvSubst (gs ++ ds)
   tcPluginTrace "Current subst" (ppr subst)
-  tcPluginTrace "wanteds" $ ppr $ map (deconsPred) ws
+  tcPluginTrace "wanteds" $ ppr $ map deconsPred ws
   tcPluginTrace "givens" $ ppr $ map (substTy subst . deconsPred) gs
   tcPluginTrace "deriveds" $ ppr $ map deconsPred ds
   let wants = mapMaybe (\ct -> (,) ct <$> toPresburgerPred subst (substTy subst $ deconsPred ct)) $
@@ -128,32 +125,28 @@
                 ]
   tcPluginTrace "prems" (text $ show $ map (toPresburgerPred subst .substTy subst . deconsPred) (gs ++ ds))
   tcPluginTrace "final goals" (text $ show $ map snd wants)
-  case testIf prems (foldr (:&&) PTrue (map snd wants)) of
+  case testIf prems (foldr ((:&&) . snd) PTrue wants) of
     Proved -> do
       tcPluginTrace "Proved" (text $ show $ map snd wants)
       return $ TcPluginOk coerced []
     Disproved wit -> do
-      tcPluginTrace "Failed! " (text $ show $ wit)
+      tcPluginTrace "Failed! " (text $ show wit)
       return $ TcPluginContradiction $ map fst wants
 
 withTyCons :: (Given MyEnv => TcPluginM a) -> TcPluginM a
 withTyCons act = do
   emd <- lookupModule (mkModuleName "Proof.Propositional.Empty") (fsLit "equational-reasoning")
-  emptyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))
-  eqcon <- getEqTyCon
-  witcon <- getEqWitnessTyCon
+  emptyClsTyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))
+  eqTyCon_ <- getEqTyCon
+  eqWitCon_ <- getEqWitnessTyCon
   pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")
-  trucon <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")
+  isTrueCon_ <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")
   vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")
   voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")
   singletons <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")
-  -- singLeqCon <- tcLookupTyCon =<< lookupOrig singletons     (mkInstTyTcOcc "<="      emptyOccSet)
-  singCompareCon <- tcLookupTyCon =<< lookupOrig singletons (mkInstTyTcOcc "Compare" emptyOccSet)
-  give (MyEnv emptyCon eqcon witcon trucon voidTyCon typeNatLeqTyCon singCompareCon) act
-
-isVoidTy :: Given MyEnv => Type -> Bool
-isVoidTy typ =                  --
-  tyConAppTyCon_maybe typ == Just (voidTyCon given)
+  typeLeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "<=")
+  singCompareCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "Compare")
+  give MyEnv{..} act
 
 (<=>) :: Prop -> Prop -> Prop
 p <=> q =  (p :&& q) :|| (Not p :&& Not q)
@@ -177,9 +170,7 @@
 
 toPresburgerPred :: Given MyEnv => TvSubst -> Type -> Maybe Prop
 toPresburgerPred subst (TyConApp con [t1, t2])
-  | con `elem` [typeNatLeqTyCon, singLeqCon] = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
--- toPresburgerPred subst (TyConApp con [t1, t2])
---   | con == singLneqCon = (:<) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
+  | con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
 toPresburgerPred subst ty
   | isEqPred ty = toPresburgerPredTree subst $ classifyPredType ty
   | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r
@@ -192,6 +183,9 @@
   , con == isTrueTyCon = toPresburgerPred subst l
   | otherwise = Nothing
 
+boolLeqs :: Given MyEnv => [TyCon]
+boolLeqs = [typeNatLeqTyCon, typeLeqBoolTyCon]
+
 toPresburgerPredTree :: Given MyEnv => TvSubst -> PredTree -> Maybe Prop
 toPresburgerPredTree subst (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True
   | Just promotedFalseDataCon  == tyConAppTyCon_maybe (substTy subst false) =
@@ -199,7 +193,7 @@
 toPresburgerPredTree subst (EqPred NomEq p b)  -- (n :<=? m) ~ 'True
   | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b)
   , Just (con, [t1, t2]) <- splitTyConApp_maybe (substTy subst p)
-  , con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1  <*> toPresburgerExp subst t2
+  , con `elem` boolLeqs = (:<=) <$> toPresburgerExp subst t1  <*> toPresburgerExp subst t2
 toPresburgerPredTree subst (EqPred NomEq p q)  -- (p :: Bool) ~ (q :: Bool)
   | typeKind p `eqType` mkTyConTy promotedBoolTyCon =
     (<=>) <$> toPresburgerPred subst p