diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Revision history for ghc-proofs
 
+## 0.1.1  -- 2017-09-05
+
+* Also run simplifier in stage 0
+
 ## 0.1  -- 2017-08-26
 
 * Initial release to hackage
diff --git a/GHC/Proof/Plugin.hs b/GHC/Proof/Plugin.hs
--- a/GHC/Proof/Plugin.hs
+++ b/GHC/Proof/Plugin.hs
@@ -128,6 +128,8 @@
                         >>= simplExpr (simplEnv in_scope 2) . occurAnalyseExpr
                         >>= simplExpr (simplEnv in_scope 1) . occurAnalyseExpr . cseOneExpr'
                         >>= simplExpr (simplEnv in_scope 1) . occurAnalyseExpr . cseOneExpr'
+                        >>= simplExpr (simplEnv in_scope 0) . occurAnalyseExpr . cseOneExpr'
+                        >>= simplExpr (simplEnv in_scope 0) . occurAnalyseExpr . cseOneExpr'
     return expr'
 
 #if  __GLASGOW_HASKELL__ >= 801
diff --git a/examples/HLint.hs b/examples/HLint.hs
--- a/examples/HLint.hs
+++ b/examples/HLint.hs
@@ -137,7 +137,7 @@
 -- -- LIST
 
 -- warn = concat (map f x) ==> concatMap f x
-proof22 f x = concat (map f x) =/= concatMap f x
+proof22 f x = concat (map f x) === concatMap f x
 
 -- warn = concat (fmap f x) ==> concatMap f x
 proof23 :: forall f. (Functor f, Foldable f) => Proof
@@ -150,7 +150,7 @@
 proof25 f g x = map f (map g x) === map (f . g) x
 
 -- hint "Fuse concatMap/map" = concatMap f (map g x) ==> concatMap (f . g) x
-proof26 f g x = concatMap f (map g x) =/= concatMap (f . g) x
+proof26 f g x = concatMap f (map g x) === concatMap (f . g) x
 
 -- hint = x !! 0 ==> head x
 proof27 x = x !! 0 =/= head x
@@ -165,8 +165,7 @@
 
 -- warn = map f (repeat x) ==> repeat (f x)
 --     where _ = noQuickCheck -- takes forever
-proof30 f x = map f (repeat x) =/= repeat (f x)
-  -- ^ works if we simplify all the way to phase 0!
+proof30 f x = map f (repeat x) === repeat (f x)
 
 -- warn = cycle [x] ==> repeat x
 --     where _ = noQuickCheck -- takes forever
@@ -220,10 +219,10 @@
 proof43 x = concatMap id x === concat x
 
 -- warn = or (map p x) ==> any p x
-proof44 p x = or (map p x) =/= any p x
+proof44 p x = or (map p x) === any p x
 
 -- warn = and (map p x) ==> all p x
-proof45 p x = and (map p x) =/= all p x
+proof45 p x = and (map p x) === all p x
 
 -- warn = zipWith (,) ==> zip
 proof46 = zipWith (,) =/= zip
@@ -249,7 +248,7 @@
 proof52 x y = not (elem x y) === notElem x y
 
 -- hint = foldr f z (map g x) ==> foldr (f . g) z x
-proof53 f z g x = foldr f z (map g x) =/= foldr (f . g) z x
+proof53 f z g x = foldr f z (map g x) === foldr (f . g) z x
 
 -- warn = x ++ concatMap (' ':) y ==> unwords (x:y)
 proof54 x y = x ++ concatMap (' ':) y =/= unwords (x:y)
diff --git a/ghc-proofs.cabal b/ghc-proofs.cabal
--- a/ghc-proofs.cabal
+++ b/ghc-proofs.cabal
@@ -1,5 +1,5 @@
 name:                ghc-proofs
-version:             0.1
+version:             0.1.1
 synopsis:            GHC plugin to prove program equations by simplification
 description:         Often when writing Haskel code, one would like to prove things about the code.
                      .