diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs
--- a/examples/simple-arith-core.hs
+++ b/examples/simple-arith-core.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -16,13 +17,18 @@
 
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806
 {-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
 #endif
 
 module Main where
 
+import Unsafe.Coerce
 import Data.Proxy
+import Numeric.Natural
 import Data.Type.Equality
 import GHC.TypeLits
+import Data.Void
 import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty)
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902
 import qualified Data.Type.Ord as DTO
@@ -31,7 +37,6 @@
 import Data.Type.Bool
 #endif
 
-
 main :: IO ()
 main = putStrLn "finished"
 
@@ -109,9 +114,10 @@
   (n <=? 2) :~: 'True
 rangeEqlLeq _ = Refl
 
+data NProxy (n :: Nat) = NProxy
+
 -- GHC >= 9.2 only Tests
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902
-data NProxy (n :: Nat) = NProxy
 
 ghc92NLeqToGt :: (n DTO.<=? m) ~ 'False 
   => NProxy n -> NProxy m -> (n DTO.>? m) :~: 'True
@@ -135,6 +141,12 @@
 
 maxLeq :: n <= m => NProxy n -> NProxy m -> DTO.Max n m :~: m
 maxLeq _ _ = Refl
+
+mkOrd :: forall n m. (n DTO.< m) => NProxy n -> NProxy m
+mkOrd _ = NProxy
+
+maxOrd :: forall n. (0 DTO.< n) => NProxy n
+maxOrd = mkOrd (NProxy @(n - 1))
 #endif
 
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904
@@ -156,3 +168,42 @@
 succGtZero :: NProxy n -> IsTrue (0 DTO.<? If (n == 0) (n + 1) n)
 succGtZero _ = Witness
 #endif
+
+succStepBack :: (Succ n <= Succ m) => NProxy n -> NProxy m -> IsTrue (n <=? m)
+succStepBack _ _ = Witness
+
+type Succ n = n + 1
+
+data Leq n m where
+  ZeroLeq :: SNat m -> Leq 0 m
+  SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1)
+
+newtype SNat n = SNat Natural
+
+data ZeroOrSucc n where
+  IsZero :: ZeroOrSucc 0
+  IsSucc ::
+    SNat n ->
+    ZeroOrSucc (n + 1)
+
+viewNat :: forall n. SNat n -> ZeroOrSucc n
+viewNat (SNat n) =
+  if n == 0
+    then unsafeCoerce IsZero
+    else unsafeCoerce (SNat (n - 1))
+
+pattern Zero :: forall n. () => n ~ 0 => SNat n
+pattern Zero <- (viewNat -> IsZero)
+
+pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n
+pattern Succ n <- (viewNat -> IsSucc n)
+
+{-# COMPLETE Zero, Succ #-}
+
+succLeqZeroAbsurd :: SNat n -> IsTrue (Succ n <=? 0) -> Void
+succLeqZeroAbsurd = undefined
+
+boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m
+boolToPropLeq Zero m = ZeroLeq m
+boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m
+boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness
diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 5bdb1784549b51d4ed7b1ae34a734767d318511c03ce6a179548a7d14f66498a
+-- hash: d6484409d9fcbd50b1fb2f56f79743a1587a1330768401bbaeecaa4e969e8160
 
 name:          ghc-typelits-presburger
-version:       0.7.0.0
+version:       0.7.1.0
 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.
@@ -75,7 +75,7 @@
   build-depends:
       base
     , equational-reasoning
-    , ghc-typelits-presburger
+    , ghc-typelits-presburger >=0.7.1.0
   default-language: Haskell2010
   if !(flag(examples))
     buildable: False
diff --git a/src/Data/Integer/SAT.hs b/src/Data/Integer/SAT.hs
--- a/src/Data/Integer/SAT.hs
+++ b/src/Data/Integer/SAT.hs
@@ -746,8 +746,6 @@
     go None xs = xs
 
 instance Monad Answer where
-  return a = One a
-
 #if !MIN_VERSION_ghc(8,8,1)
   fail _             = None
 #endif
@@ -771,13 +769,12 @@
   fmap f (Choice x1 x2) = Choice (fmap f x1) (fmap f x2)
 
 instance Applicative Answer where
-  pure = return
+  pure = One
   (<*>) = ap
 
 newtype S a = S (RW -> Answer (a, RW))
 
 instance Monad S where
-  return a = S $ \s -> return (a, s)
   S m >>= k = S $ \s -> do
     (a, s1) <- m s
     let S m1 = k a
@@ -795,7 +792,7 @@
   fmap = liftM
 
 instance Applicative S where
-  pure = return
+  pure a = S $ \s -> pure (a, s)
   (<*>) = ap
 
 updS :: (RW -> (a, RW)) -> S a
diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs
--- a/src/GHC/TypeLits/Presburger/Compat.hs
+++ b/src/GHC/TypeLits/Presburger/Compat.hs
@@ -13,6 +13,11 @@
 import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS)
 #if MIN_VERSION_ghc(9,4,1)
 import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..))
+import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (cTupleTyCon, cTupleDataCon)
+import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (evCast)
+import GHC.Plugins as GHC.TypeLits.Presburger.Compat (mkUnivCo)
+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (UnivCoProvenance(..))
+import GHC.Core.DataCon as GHC.TypeLits.Presburger.Compat (dataConWrapId)
 #else
 import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..))
 #endif
diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs
--- a/src/GHC/TypeLits/Presburger/Types.hs
+++ b/src/GHC/TypeLits/Presburger/Types.hs
@@ -16,6 +16,8 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 -- | Since 0.3.0.0
 module GHC.TypeLits.Presburger.Types
   ( pluginWith,
@@ -40,6 +42,9 @@
 import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName)
 import qualified Data.Integer.SAT as SAT
 import Data.List (nub)
+#if MIN_VERSION_ghc(9,4,0)
+import qualified GHC.Core as GHC (Expr(..))
+#endif
 import qualified Data.List as L
 import qualified Data.Map.Strict as M
 import Data.Maybe
@@ -51,7 +56,7 @@
   )
 import Data.Reflection (Given, give, given)
 import qualified Data.Set as Set
-import GHC.TypeLits.Presburger.Compat
+import GHC.TypeLits.Presburger.Compat as Compat
 import qualified Data.Foldable as F
 
 assert' :: Prop -> PropSet -> PropSet
@@ -333,9 +338,9 @@
       return (prems, map (second $ handleSubtraction mode) wants, catMaybes resls)
     let solved = map fst $ filter (isProved . testIf prems . snd) wants
         coerced =
-          [ (evByFiat "ghc-typelits-presburger" t1 t2, ct)
+          [ (evProof, ct)
           | ct <- solved
-          , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)
+          , Just evProof <- pure $ extractProof $ classifyPredType $ deconsPred ct
           ]
     tcPluginTrace "pres: final premises" (text $ show prems0)
     tcPluginTrace "pres: final goals" (text $ show $ map snd wants)
@@ -348,6 +353,23 @@
         tcPluginTrace "pres: Failed! " (text $ show wit)
         return $ TcPluginContradiction $ map fst wants
 
+
+extractProof :: Given Translation => PredTree -> Maybe EvTerm
+extractProof (EqPred NomEq t1 t2) = 
+    Just $ evByFiat "ghc-typelits-presburger" t1 t2
+#if MIN_VERSION_base(4,17,0)
+extractProof (IrredPred prd)
+  | Just (con, lastN 2 -> [_, _]) <- splitTyConApp_maybe prd
+  , con `elem` assertTy given = 
+    Just $ GHC.Var (dataConWrapId $ cTupleDataCon 0) `evCast`
+      mkUnivCo
+      (PluginProv $ "ghc-typelits-presburger: extractProof")
+      Representational
+      (mkTyConTy (cTupleTyCon 0))
+      prd
+#endif
+extractProof _ = Nothing
+
 eqReasoning :: FastString
 eqReasoning = fsLit "equational-reasoning"
 
@@ -721,7 +743,7 @@
 #else
 simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2)
 #endif
-#endif
+#endif 
 simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2)
 simpleExp (TyConApp tc (lastTwo -> ts)) =
   fromMaybe (TyConApp tc (map simpleExp ts)) $