diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
--- a/Data/Type/Natural.hs
+++ b/Data/Type/Natural.hs
@@ -151,9 +151,7 @@
 
 reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n :== m)
 reflToSEqual SZ     _      Refl = Witness
-reflToSEqual (SS n) (SS m) Refl =
-  case reflToSEqual n m Refl of
-    Witness -> Witness
+reflToSEqual (SS n) (SS m) Refl = reflToSEqual n m Refl
 reflToSEqual (SS _) SZ refl = case refl of {}
 
 sequalToRefl :: SNat n -> SNat m -> IsTrue (n :== m) -> n :~: m
@@ -170,35 +168,27 @@
 sequalSym SZ SZ         = Refl
 sequalSym SZ (SS _)     = Refl
 sequalSym (SS _) SZ     = Refl
-sequalSym (SS n) (SS m) =
-  case sequalSym n m of
-    Refl -> Refl
+sequalSym (SS n) (SS m) = sequalSym n m
 
 sleqFlip :: SNat n -> SNat m -> (n :~: m -> Void) -> (m :<= n) :~: Not (n :<= m)
 sleqFlip SZ     SZ     neq = absurd $ neq Refl
 sleqFlip SZ     (SS _) _   = Refl
 sleqFlip (SS _) SZ     _   = Refl
-sleqFlip (SS n) (SS m) neq =
-  case sleqFlip n m (neq . succCong) of
-    Refl -> Refl
+sleqFlip (SS n) (SS m) neq = sleqFlip n m (neq . succCong)
 
 sLeqReflexive :: SNat n -> SNat m -> IsTrue (n :== m) -> IsTrue (n :<= m)
 sLeqReflexive SZ     _      Witness = Witness
-sLeqReflexive (SS n) (SS m) Witness =
-  case sLeqReflexive n m Witness of
-    Witness -> Witness
+sLeqReflexive (SS n) (SS m) Witness = sLeqReflexive n m Witness
 sLeqReflexive (SS _) SZ  witness = case witness of {}
 
 nonSLeqToLT :: (n :<= m) ~ 'False => SNat n -> SNat m -> Compare m n :~: 'LT
-nonSLeqToLT n m =
-  case sequalSym n m of
-    Refl -> 
-      case m %:== n of
-        STrue -> case sLeqReflexive n m Witness of {}
-        SFalse ->
-          case m %:<= n of
-            STrue  -> Refl
-            SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {}
+nonSLeqToLT n m = withRefl (sequalSym n m) $
+  case m %:== n of
+    STrue -> case sLeqReflexive n m Witness of {}
+    SFalse ->
+      case m %:<= n of
+        STrue  -> Refl
+        SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {}
 
 instance PeanoOrder Nat where
   {-# SPECIALISE instance PeanoOrder Nat #-}
@@ -229,20 +219,15 @@
 
   flipCompare n m =
     case n %:== m of
-      STrue ->  case sequalSym n m of
-        Refl -> Refl
-      SFalse ->
-        case sequalSym n m of
-          Refl -> 
-            case n %:<= m of
-              STrue ->
-                case sleqFlip n m (snequalToNoRefl n m Witness) of
-                  Refl -> case m %:<= n of
-                    SFalse -> Refl
-              SFalse ->
-                case sleqFlip n m (snequalToNoRefl n m Witness) of
-                  Refl -> case m %:<= n of
-                    STrue -> Refl
+      STrue -> withRefl (sequalSym n m) Refl
+      SFalse -> withRefl (sequalSym n m) $
+        case n %:<= m of
+          STrue -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $
+            case m %:<= n of
+              SFalse -> Refl
+          SFalse -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $
+            case m %:<= n of
+              STrue -> Refl
 
   minLeqL SZ SZ     = Witness
   minLeqL SZ (SS _) = Witness
diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs
--- a/Data/Type/Natural/Builtin.hs
+++ b/Data/Type/Natural/Builtin.hs
@@ -46,10 +46,10 @@
 import           Data.Void                    (Void)
 import           GHC.TypeLits                 (type (+), type (<=), type (<=?))
 import qualified GHC.TypeLits                 as TL
-import           Proof.Equational             (coerce)
+import           Proof.Equational             (coerce, withRefl)
 import           Proof.Equational             (start, sym, (===), (=~=))
 import           Proof.Equational             (because)
-import           Proof.Propositional          (Empty (..), IsTrue (..))
+import           Proof.Propositional          (Empty (..), IsTrue (..), withWitness)
 import           Unsafe.Coerce                (unsafeCoerce)
 
 -- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@.
@@ -66,7 +66,7 @@
 viewNat :: Sing (n :: TL.Nat) -> ZeroOrSucc n
 viewNat n =
   case n %~ (sing :: Sing 0) of
-    Proved Refl -> IsZero
+    Proved _    -> IsZero
     Disproved _ -> IsSucc (sPred n)
 
 sFromPeano :: Sing n -> Sing (FromPeano n)
@@ -88,7 +88,7 @@
 sToPeano :: Sing n -> Sing (ToPeano n)
 sToPeano sn =
   case sn %~ (sing :: Sing 0) of
-    Proved Refl  -> SZ
+    Proved eq     -> withRefl eq SZ
     Disproved _pf -> coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn)))
 
 -- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat).
@@ -258,9 +258,9 @@
                 => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True
 toPeanoMonotone sn sm =
   case sn %~ (sing :: Sing 0) of
-    Proved Refl -> Refl
+    Proved eql -> withRefl eql Refl
     Disproved nPos -> case sm %~ (sing :: Sing 0) of
-      Proved Refl -> absurd $ nPos $ natLeqZero sn
+      Proved _ -> absurd $ nPos $ natLeqZero sn
       Disproved mPos ->
         let pn = sPred sn
             pm = sPred sm
@@ -367,25 +367,25 @@
   leqToMax _ _ Witness = Refl
   geqToMax n m mLEQn =
     case leqToCmp m n mLEQn of
-      Left Refl  -> Refl
+      Left eql   -> withRefl eql Refl
       Right mLTn ->
         maxCompareFlip n m mLTn
   geqToMin n m mLEQn =
     case leqToCmp m n mLEQn of
-      Left Refl  -> Refl
+      Left eql   -> withRefl eql Refl
       Right mLTn ->
         minCompareFlip n m mLTn
 
   lneqReversed n m =
-    case flipCompare n m of
-      Refl -> case sCompare n m of
+    withRefl (flipCompare n m) $
+      case sCompare n m of
         SEQ -> Refl
         SLT -> Refl
         SGT -> Refl
 
   leqReversed n m =
-    case flipCompare n m of
-      Refl -> case sCompare n m of
+    withRefl (flipCompare n m) $
+      case sCompare n m of
         SEQ -> Refl
         SLT -> Refl
         SGT -> Refl
@@ -397,12 +397,10 @@
           =~= SFalse
           === (sSucc n %:<= n) `because` sym (succLeqAbsurd' n)
           === (sSucc n %:<= m) `because` sLeqCongR (sSucc n) (eqToRefl n m Refl)
-      SLT ->
-        case ltToSuccLeq n m Refl of
-          Witness ->
-            start (n %:< m)
-              =~= STrue
-              =~= (sSucc n %:<= m)
+      SLT -> withWitness (ltToSuccLeq n m Refl) $
+        start (n %:< m)
+          =~= STrue
+          =~= (sSucc n %:<= m)
       SGT ->
         case sSucc n %:<= m of
           SFalse -> Refl
diff --git a/Data/Type/Natural/Class/Order.hs b/Data/Type/Natural/Class/Order.hs
--- a/Data/Type/Natural/Class/Order.hs
+++ b/Data/Type/Natural/Class/Order.hs
@@ -249,7 +249,7 @@
            -> Compare a b :~: 'LT
   leqToLT n m snLEQm =
     case leqToCmp (sSucc n) m snLEQm of
-      Left Refl ->
+      Left eql -> withRefl eql $
         start (sCompare n m)
           =~= sCompare n (sSucc n)
           === SLT `because` ltSucc n
@@ -264,7 +264,7 @@
   leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (Succ n :<= Succ m)
   leqSucc n m nLEQm =
     case leqToCmp n m nLEQm of
-      Left  Refl  -> leqRefl (sSucc n)
+      Left  eql  -> withRefl eql $ leqRefl (sSucc n)
       Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm
 
   fromLeqView :: LeqView (n :: nat) m -> IsTrue (n :<= m)
@@ -470,9 +470,7 @@
   leqSucc' :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (Succ n :<= Succ m)
   leqSucc' n m =
     case n %:<= m of
-      STrue ->
-        case leqSucc n m Witness of
-          Witness -> Refl
+      STrue -> withWitness (leqSucc n m Witness) Refl
       SFalse ->
         case sSucc n %:<= sSucc m of
           SFalse -> Refl
diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -53,8 +53,8 @@
 fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n :< Succ m) ~ 'True, SingI m)
         => Sing (n :: nat) -> Ordinal m
 fromOLt  n =
-  case coerce (sym $ succLneqSucc n (sing :: Sing m)) Witness of
-    Witness -> OLt n
+  withRefl (sym $ succLneqSucc n (sing :: Sing m)) $
+  OLt n
 
 -- | Pattern synonym representing the 0-th ordinal.
 pattern OZ :: forall nat (n :: nat). IsPeano nat
@@ -135,32 +135,31 @@
 
 enumOrdinal :: (PeanoOrder nat, SingI n) => Sing (n :: nat) -> [Ordinal n]
 enumOrdinal (Succ n) = withSingI n $
-  case lneqZero n of
-    Witness ->
+  withWitness (lneqZero n) $
       OLt sZero : map succOrd (enumOrdinal n)
 enumOrdinal _ = []
 
 succOrd :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n)
 succOrd (OLt n) =
-  case succLneqSucc n (sing :: Sing n) of
-    Refl -> OLt (sSucc n)
+  withRefl (succLneqSucc n (sing :: Sing n)) $
+  OLt (sSucc n)
 {-# INLINE succOrd #-}
 
 instance SingI n => Bounded (Ordinal ('PN.S n)) where
   minBound = OLt PN.SZ
 
   maxBound =
-    case leqRefl (sing :: Sing n) of
-      Witness -> sNatToOrd (sing :: Sing n)
+    withWitness (leqRefl (sing :: Sing n)) $
+    sNatToOrd (sing :: Sing n)
 
 instance (SingI m, SingI n, n ~ (m + 1)) => Bounded (Ordinal n) where
   minBound =
-    case lneqZero (sing :: Sing m) of
-      Witness -> OLt (sing :: Sing 0)
+    withWitness (lneqZero (sing :: Sing m)) $
+    OLt (sing :: Sing 0)
   {-# INLINE minBound #-}
   maxBound =
-    case lneqSucc (sing :: Sing m) of
-      Witness -> sNatToOrd (sing :: Sing m)
+    withWitness (lneqSucc (sing :: Sing m)) $
+    sNatToOrd (sing :: Sing m)
   {-# INLINE maxBound #-}
 
 
@@ -232,8 +231,7 @@
      => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
 OLt k @+ OLt l =
   let (n, m) = (n :: Sing n, m :: Sing m)
-  in case plusStrictMonotone k n l m Witness Witness of
-    Witness -> OLt $ k %:+ l
+  in withWitness (plusStrictMonotone k n l m Witness Witness) $ OLt $ k %:+ l
 
 -- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value.
 --
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                type-natural
-version:             0.6.1.0
+version:             0.6.1.1
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
                      .
@@ -39,7 +39,7 @@
                      , Data.Type.Natural.Core
                      , Data.Type.Natural.Compat
   build-depends:       base                      >= 4       && < 5
-                     , equational-reasoning      >= 0.4.1   && < 1
+                     , equational-reasoning      >= 0.4.1.1 && < 1
                      , monomorphic               >= 0.0.3
                      , template-haskell          >= 2.8     && < 3
                      , constraints               >= 0.3     && < 0.9