diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Change Log
 
+## 0.1.5
+
+* Bump dependencies, fix equality, tweak readme
+
 ## 0.1.4
 
 * Bump dependencies
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/expressions.cabal b/expressions.cabal
--- a/expressions.cabal
+++ b/expressions.cabal
@@ -1,5 +1,5 @@
 name:                expressions
-version:             0.1.4
+version:             0.1.5
 synopsis:            Expressions and Formulae a la carte
 description:
   This package is aimed at providing means of fixing a first-order language and
@@ -71,10 +71,10 @@
                        TypeSynonymInstances,
                        UndecidableInstances
   build-depends:       attoparsec >=0.13 && <0.14,
-                       base >=4.9 && <4.11,
-                       containers >=0.5.7 && <0.5.11,
+                       base >=4.9 && <4.12,
+                       containers >=0.5.7 && <0.6,
                        lattices >=1.6 && <1.8,
-                       singletons >=2.2 && <2.4,
+                       singletons >=2.2 && <2.5,
                        text >=1.2 && <1.3,
                        transformers >=0.5.2 && <0.6
   hs-source-dirs:      src
@@ -86,10 +86,7 @@
   build-depends:       base,
                        expressions,
                        singletons,
-                       text,
-                       tasty,
-                       tasty-quickcheck,
-                       QuickCheck >=2.10 && <2.11
+                       text
   hs-source-dirs:      test
   main-is:             Main.hs
   default-language:    Haskell2010
diff --git a/src/Data/Expression/Arithmetic.hs b/src/Data/Expression/Arithmetic.hs
--- a/src/Data/Expression/Arithmetic.hs
+++ b/src/Data/Expression/Arithmetic.hs
@@ -53,9 +53,10 @@
     LessThan :: a 'IntegralSort -> a 'IntegralSort -> ArithmeticF a 'BooleanSort
 
 instance IEq1 ArithmeticF where
-    Const a  `ieq1` Const b  = a == b
-    Add   as `ieq1` Add   bs = foldr (&&) True $ zipWith ieq as bs
-    Mul   as `ieq1` Mul   bs = foldr (&&) True $ zipWith ieq as bs
+    Const a  `ieq1` Const b = a == b
+
+    Add as `ieq1` Add bs | length as == length bs = foldr (&&) True $ zipWith ieq as bs
+    Mul as `ieq1` Mul bs | length as == length bs = foldr (&&) True $ zipWith ieq as bs
 
     Divides  c a `ieq1` Divides  d b = a `ieq` b && c == d
     LessThan a c `ieq1` LessThan b d = a `ieq` b && c `ieq` d
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,26 +1,47 @@
 {-# LANGUAGE DataKinds
+           , FlexibleContexts
            , KindSignatures
            , OverloadedStrings
            , RankNTypes
            , TypeOperators #-}
 
+import Control.Monad
 import Data.Maybe
 import Data.Singletons
 import Data.Text
 import Prelude hiding (and)
-import Test.QuickCheck hiding ((.&.))
-import Test.Tasty
-import Test.Tasty.QuickCheck hiding ((.&.))
 
+import qualified Prelude as P
+
 import Data.Expression
 
 parseJust :: forall f (s :: Sort). ( Parseable f f, SingI s ) => Text -> IFix f s
 parseJust = fromJust . parse
 
+a, b, x, y, z :: forall f (s :: Sort). ( VarF :<: f, SingI s ) => IFix f s
+a = var "a"
+b = var "b"
+x = var "x"
+y = var "y"
+z = var "z"
+
+c1, c3 :: forall f. ArithmeticF :<: f => IFix f 'IntegralSort
+c1 = cnst 1
+c3 = cnst 3
+
 main :: IO ()
-main = defaultMain $ testGroup "parsing" [ testProperty "1" $ once $ var "a" == (parseJust "(a : int)" :: ALia 'IntegralSort)
-                                         , testProperty "2" $ once $ var "a" /= (parseJust "(+ (a : int) 3)" :: ALia 'IntegralSort)
-                                         , testProperty "3" $ once $ var "a" .+. cnst 1 == (parseJust "(+ (a : int) 1)" :: ALia 'IntegralSort)
-                                         , testProperty "4" $ once $ select (var "a") (var "b" .+. cnst 3) == (parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))" :: QFALia ('ArraySort 'IntegralSort 'BooleanSort))
-                                         , testProperty "5" $ once $ forall [var "x" :: Var 'IntegralSort] (exists [var "y" :: Var 'IntegralSort] (and [true, var "b" .=. (var "x" .<. var "y")])) == (parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))" :: Lia 'BooleanSort)
-                                         , testProperty "6" $ once $ forall [var "x" :: Var 'IntegralSort, var "y"] (var "x" .<. var "y" .+. var "z") .&. var "z" .=. cnst 3 == (parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))" :: Lia 'BooleanSort) ]
+main = guard (P.and props) where
+
+    props = [ e1 == (parseJust "(a : int)"                                                                   :: ALia 'IntegralSort)
+            , e2 /= (parseJust "(+ (a : int) 3)"                                                             :: ALia 'IntegralSort)
+            , e3 == (parseJust "(+ (a : int) 1)"                                                             :: ALia 'IntegralSort)
+            , e4 == (parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))"                   :: QFALia ('ArraySort 'IntegralSort 'BooleanSort))
+            , e5 == (parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))" :: Lia 'BooleanSort)
+            , e6 == (parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"          :: Lia 'BooleanSort) ]
+
+    e1 = a
+    e2 = a
+    e3 = a .+. c1
+    e4 = select a (b .+. c3)
+    e5 = forall [x :: Var 'IntegralSort] (exists [y :: Var 'IntegralSort] (and [true, b .=. (x .<. y)]))
+    e6 = forall [x :: Var 'IntegralSort, y] (x .<. y .+. z) .&. z .=. c3