diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.5.5 *October 22nd 2017*
+* Solve inequalities when their normal forms are the same, i.e.
+  * `(2 <= (2 ^ (n + d)))` implies `(2 <= (2 ^ (d + n)))`
+* Find more unifications:
+  * `8^x - 2*4^x ~ 8^y - 2*4^y ==> [x := y]`
+
 ## 0.5.4 *October 14th 2017*
 * Perform normalisations such as: `2^x * 4^x ==> 8^x`
 
diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal
--- a/ghc-typelits-natnormalise.cabal
+++ b/ghc-typelits-natnormalise.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-natnormalise
-version:             0.5.4
+version:             0.5.5
 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat
 description:
   A type checker plugin for GHC that can solve /equalities/ of types of kind
diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs
--- a/src/GHC/TypeLits/Normalise.hs
+++ b/src/GHC/TypeLits/Normalise.hs
@@ -52,6 +52,7 @@
 -- external
 import Control.Arrow       (second)
 import Control.Monad       (replicateM)
+import Data.Either         (rights)
 import Data.List           (intersect)
 import Data.Maybe          (mapMaybe)
 import GHC.TcPluginM.Extra (tracePlugin)
@@ -116,7 +117,7 @@
       [] -> return (TcPluginOk [] [])
       _  -> do
         unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens
-        sr <- simplifyNats (unit_givens ++ unit_wanteds)
+        sr <- simplifyNats unit_givens unit_wanteds
         tcPluginTrace "normalised" (ppr sr)
         case sr of
           Simplified evs -> do
@@ -140,10 +141,15 @@
   ppr (Simplified evs) = text "Simplified" $$ ppr evs
   ppr (Impossible eq)  = text "Impossible" <+> ppr eq
 
-simplifyNats :: [Either NatEquality NatInEquality]
-             -> TcPluginM SimplifyResult
-simplifyNats eqs =
-    tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs
+simplifyNats
+  :: [Either NatEquality NatInEquality]
+  -- ^ Given constraints
+  -> [Either NatEquality NatInEquality]
+  -- ^ Wanted constraints
+  -> TcPluginM SimplifyResult
+simplifyNats eqsG eqsW =
+    let eqs = eqsG ++ eqsW
+    in  tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs
   where
     simples :: [CoreUnify]
             -> [((EvTerm, Ct), [Ct])]
@@ -175,7 +181,15 @@
           evs' <- maybe evs (:evs) <$> evMagic ct []
           simples subst evs' xs eqs'
         Just False -> return (Impossible eq)
-        Nothing    -> simples subst evs (eq:xs) eqs'
+        Nothing    ->
+          -- This inequality is either a given constraint, or it is a wanted
+          -- constraint, which in normal form is equal to another given
+          -- constraint, hence it can be solved.
+          if u `elem` (map snd (rights eqsG))
+             then do
+               evs' <- maybe evs (:evs) <$> evMagic ct []
+               simples subst evs' xs eqs'
+             else simples subst evs (eq:xs) eqs'
 
 -- Extract the Nat equality constraints
 toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality)
diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
--- a/src/GHC/TypeLits/Normalise/Unify.hs
+++ b/src/GHC/TypeLits/Normalise/Unify.hs
@@ -38,7 +38,7 @@
 
 -- External
 import Data.Function (on)
-import Data.List     ((\\), intersect, mapAccumL)
+import Data.List     ((\\), intersect, mapAccumL, nub)
 
 import GHC.Base               (isTrue#,(==#))
 import GHC.Integer            (smallInteger)
@@ -175,6 +175,7 @@
                    | UnifyItem { siLHS  :: SOP v c
                                , siRHS  :: SOP v c
                                }
+  deriving Eq
 
 instance (Outputable v, Outputable c) => Outputable (UnifyItem v c) where
   ppr (SubstItem {..}) = ppr siVar <+> text " := " <+> ppr siSOP
@@ -388,7 +389,9 @@
 
 -- (a + c) ~ (b + c) ==> [a := b]
 unifiers' ct (S ps1)       (S ps2)
-    | null psx  = unifiers'' ct (S ps1) (S ps2)
+    | null psx  = case zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2 of
+                    [] -> unifiers'' ct (S ps1) (S ps2)
+                    ks -> nub (concat ks)
     | otherwise = unifiers' ct (S ps1'') (S ps2'')
   where
     ps1'  = ps1 \\ psx
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -248,9 +248,24 @@
 proxyInEq5 :: Proxy 1 -> Proxy (2^a) -> ()
 proxyInEq5 = proxyInEq
 
-proxyEq1 :: Proxy x -> Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1)))
-proxyEq1 _ = id
+proxyEq1 :: Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1)))
+proxyEq1 = id
 
+proxyEq2 :: Proxy (((2 ^ x) - 2) * (2 ^ (x + x))) -> Proxy ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))
+proxyEq2 = id
+
+proxyInEqImplication :: (2 <= (2 ^ (n + d)))
+  => Proxy d
+  -> Proxy n
+  -> Proxy n
+proxyInEqImplication = proxyInEqImplication'
+
+proxyInEqImplication' :: (2 <= (2 ^ (d + n)))
+  => Proxy d
+  -> Proxy n
+  -> Proxy n
+proxyInEqImplication' _ = id
+
 main :: IO ()
 main = defaultMain tests
 
@@ -290,8 +305,11 @@
     ]
   , testGroup "Equality"
     [ testCase "((2 ^ x) * (2 ^ (x + x))) ~ (2 * (2 ^ ((x + (x + x)) - 1)))" $
-      show (proxyEq1 (Proxy :: Proxy 4) Proxy) @?=
+      show (proxyEq1 Proxy) @?=
       "Proxy"
+    , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $
+      show (proxyEq2 Proxy) @?=
+      "Proxy"
     ]
   , testGroup "Inequality"
     [ testCase "a <= a+1" $
@@ -309,6 +327,9 @@
     , testCase "1 <= 2^a" $
       show (proxyInEq5 (Proxy :: Proxy 1) (Proxy :: Proxy 1)) @?=
       "()"
+    , testCase "`(2 <= (2 ^ (n + d)))` implies `(2 <= (2 ^ (d + n)))`" $
+      show (proxyInEqImplication (Proxy :: Proxy 3) (Proxy :: Proxy 4)) @?=
+      "Proxy"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors