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.4.1 *February 4th 2016*
+* Find more unifications:
+  * `F x y k z ~ F x y (k-1+1) z` ==> [k := k], where `F` can be any type function
+
 ## 0.4 *January 19th 2016*
 * Stop using 'provenance' hack to create conditional evidence (GHC 8.0+ only)
 * Find more unifications:
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# ghc-tynat-normalise
+# ghc-typelits-natnormalise
 
 [![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-natnormalise.png?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise)
 [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-natnormalise.svg)](https://hackage.haskell.org/package/ghc-typelits-natnormalise)
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.4
+version:             0.4.1
 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
@@ -55,6 +55,7 @@
 
 -- external
 import Data.IORef          (IORef, newIORef,readIORef, modifyIORef)
+import Data.List           (intersect)
 import Data.Maybe          (catMaybes, mapMaybe)
 import GHC.TcPluginM.Extra (evByFiat, newGiven, tracePlugin)
 
@@ -81,6 +82,13 @@
 import TcType              (mkEqPred, typeKind)
 import GHC.TcPluginM.Extra (newWantedWithProvenance, failWithProvenace)
 #endif
+#if __GLASGOW_HASKELL__ >= 711
+import TyCoRep       (Type (..))
+#else
+import TypeRep       (Type (..))
+#endif
+import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
+                      typeNatSubTyCon)
 
 
 -- internal
@@ -250,10 +258,23 @@
 toNatEquality :: Ct -> Maybe NatEquality
 toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
     EqPred NomEq t1 t2
-      | isNatKind (typeKind t1) || isNatKind (typeKind t1)
-      -> Just (ct,normaliseNat t1,normaliseNat t2)
+      -> go t1 t2
     _ -> Nothing
   where
+    go (TyConApp tc xs) (TyConApp tc' ys)
+      | tc == tc'
+      , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon
+                                   ,typeNatMulTyCon,typeNatExpTyCon])
+      = case filter (uncurry (/=)) (zip xs ys) of
+          [(x,y)] | isNatKind (typeKind x) &&  isNatKind (typeKind y)
+                  -> Just (ct, normaliseNat x, normaliseNat y)
+          _ -> Nothing
+    go x y
+      | isNatKind (typeKind x) && isNatKind (typeKind y)
+      = Just (ct,normaliseNat x,normaliseNat y)
+      | otherwise
+      = Nothing
+
     isNatKind :: Kind -> Bool
     isNatKind = (== typeNatKind)