diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.5.6 *October 31st 2017*
+* Fixes bugs:
+  * `(x + 1) ~ (2 * y)` no longer implies `((2 * (y - 1)) + 1) ~ x`
+
 ## 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)))`
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.5
+version:             0.5.6
 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/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
--- a/src/GHC/TypeLits/Normalise/Unify.hs
+++ b/src/GHC/TypeLits/Normalise/Unify.hs
@@ -389,9 +389,9 @@
 
 -- (a + c) ~ (b + c) ==> [a := b]
 unifiers' ct (S ps1)       (S ps2)
-    | null psx  = case zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2 of
+    | null psx  = case concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) of
                     [] -> unifiers'' ct (S ps1) (S ps2)
-                    ks -> nub (concat ks)
+                    ks -> nub 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
@@ -254,6 +254,15 @@
 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
 
+proxyEq3
+  :: forall x y
+   . ((x + 1) ~ (2 * y))
+  => Proxy x
+  -> Proxy y
+  -> Proxy (((2 * (y - 1)) + 1))
+  -> Proxy x
+proxyEq3 _ _ x = x
+
 proxyInEqImplication :: (2 <= (2 ^ (n + d)))
   => Proxy d
   -> Proxy n
@@ -309,6 +318,11 @@
       "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 "Implications"
+    [ testCase "(x + 1) ~ (2 * y)) implies (((2 * (y - 1)) + 1)) ~ x" $
+      show (proxyEq3 (Proxy :: Proxy 3) (Proxy :: Proxy 2) Proxy) @?=
       "Proxy"
     ]
   , testGroup "Inequality"