diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2015, mniip
+Copyright (c) 2015-2022, mniip
 
 All rights reserved.
 
diff --git a/finite-typelits.cabal b/finite-typelits.cabal
--- a/finite-typelits.cabal
+++ b/finite-typelits.cabal
@@ -1,5 +1,5 @@
 name:                finite-typelits
-version:             0.1.5.0
+version:             0.1.6.0
 synopsis:            A type inhabited by finitely many values, indexed by type-level naturals
 description:         A type inhabited by finitely many values, indexed by type-level naturals.
 homepage:            https://github.com/mniip/finite-typelits
@@ -14,7 +14,7 @@
 library
   exposed-modules:     Data.Finite
                      , Data.Finite.Internal
-  build-depends:       base >= 4.7 && <= 4.17
+  build-depends:       base >= 4.7 && < 4.18
                      , deepseq >= 1.4
   hs-source-dirs:      src
   default-language:    Haskell2010
@@ -24,7 +24,7 @@
   type:                exitcode-stdio-1.0
   main-is:             test/Main.hs
   build-depends:       finite-typelits
-                     , base >= 4.9 && <= 4.17
+                     , base >= 4.9 && < 4.18
                      , deepseq >= 1.4
                      , QuickCheck
   default-language:    Haskell2010
diff --git a/src/Data/Finite.hs b/src/Data/Finite.hs
--- a/src/Data/Finite.hs
+++ b/src/Data/Finite.hs
@@ -117,14 +117,14 @@
 
 -- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input
 -- was one of the removed inhabitants.
-strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n)
+strengthenN :: KnownNat n => Finite m -> Maybe (Finite n)
 strengthenN (Finite x) = result
     where
         result = if x < natVal (fromJust result)
             then Just $ Finite x
             else Nothing
 
--- | Add multiple inhabitant in the beginning, shifting everything up by the
+-- | Add multiple inhabitants in the beginning, shifting everything up by the
 -- amount of inhabitants added.
 shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m
 shiftN fx@(Finite x) = result
@@ -134,7 +134,7 @@
 -- | Remove multiple inhabitants from the beginning, shifting everything down by
 -- the amount of inhabitants removed. Returns 'Nothing' if the input was one of
 -- the removed inhabitants.
-unshiftN :: (KnownNat n, KnownNat m, n <= m) => Finite m -> Maybe (Finite n)
+unshiftN :: (KnownNat n, KnownNat m) => Finite m -> Maybe (Finite n)
 unshiftN fx@(Finite x) = result
     where
         result = if x < natVal fx - natVal (fromJust result)
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -320,15 +320,13 @@
         n <= m ==> unsafeWithInequality @n @m @Property $
             map (weakenN @n @m) finites === take n finites
 
-prop_valid_strengthenN = withNat $ \n (_ :: Proxy n) ->
-    withNatPos $ \m (_ :: Proxy m) ->
-        n <= m ==> unsafeWithInequality @n @m @Property $
-            property $ \x ->
-                maybe True isValidFinite $ strengthenN @n @m x
+prop_valid_strengthenN = withNat $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x ->
+            maybe True isValidFinite $ strengthenN @n @m x
 prop_finites_strengthenN = withNat $ \n (_ :: Proxy n) ->
     withNat $ \m (_ :: Proxy m) ->
-        n <= m ==> unsafeWithInequality @m @n @Property $
-            map (strengthenN @m @n) finites === take n (map Just finites) ++ replicate (n - m) Nothing
+        map (strengthenN @m @n) finites === take n (map Just finites) ++ replicate (n - m) Nothing
 
 prop_valid_shiftN = withNatPos $ \n (_ :: Proxy n) ->
     withNatPos $ \m (_ :: Proxy m) ->
@@ -340,15 +338,13 @@
         n <= m ==> unsafeWithInequality @n @m @Property $
             map (shiftN @n @m) finites === drop (m - n) finites
 
-prop_valid_unshiftN = withNatPos $ \n (_ :: Proxy n) ->
-    withNat $ \m (_ :: Proxy m) ->
-        n <= m ==> unsafeWithInequality @n @m @Property $
-            property $ \x ->
-                maybe True isValidFinite $ unshiftN @n @m x
+prop_valid_unshiftN = withNatPos $ \_ (_ :: Proxy n) ->
+    withNat $ \_ (_ :: Proxy m) ->
+        property $ \x ->
+            maybe True isValidFinite $ unshiftN @n @m x
 prop_finites_unshiftN = withNat $ \n (_ :: Proxy n) ->
     withNat $ \m (_ :: Proxy m) ->
-        m <= n ==> unsafeWithInequality @m @n @Property $
-            map (unshiftN @m @n) finites === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)
+        map (unshiftN @m @n) finites === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)
 
 prop_valid_weakenProxy = withNatPos $ \n (_ :: Proxy n) ->
     withNat $ \k (_ :: Proxy k) ->