diff --git a/Test/LazySmallCheck.hs b/Test/LazySmallCheck.hs
--- a/Test/LazySmallCheck.hs
+++ b/Test/LazySmallCheck.hs
@@ -7,6 +7,7 @@
   , Cons           -- :: *
   , cons           -- :: a -> Series a
   , (><)           -- :: Series (a -> b) -> Series a -> Series b
+  , empty          -- :: Series a
   , (\/)           -- :: Series a -> Series a -> Series a
   , drawnFrom      -- :: [a] -> Cons a
   , cons0          -- :: a -> Series a
@@ -17,14 +18,16 @@
   , cons5          -- :: ...
   , Testable       -- :: class
   , depthCheck     -- :: Testable a => Int -> a -> IO ()
+  , smallCheck     -- :: Testable a => Int -> a -> IO ()
   , test           -- :: Testable a => a -> IO ()
   , (==>)          -- :: Bool -> Bool -> Bool
-  , Prop           -- :: *
-  , lift           -- :: Bool -> Prop
-  , neg            -- :: Prop -> Prop
-  , (*&*)          -- :: Prop -> Prop -> Prop
-  , (*|*)          -- :: Prop -> Prop -> Prop
-  , (*=>*)         -- :: Prop -> Prop -> Prop
+  , Property       -- :: *
+  , lift           -- :: Bool -> Property
+  , neg            -- :: Property -> Property
+  , (*&*)          -- :: Property -> Property -> Property
+  , (*|*)          -- :: Property -> Property -> Property
+  , (*=>*)         -- :: Property -> Property -> Property
+  , (*=*)          -- :: Property -> Property -> Property
   )
   where
 
@@ -54,13 +57,20 @@
 cons :: a -> Series a
 cons a d = C (SumOfProd [[]]) [const a]
 
+empty :: Series a
+empty d = C (SumOfProd []) []
+
 (><) :: Series (a -> b) -> Series a -> Series b
-(f >< a) d = C (SumOfProd [ta:p | d > 0, p <- ps]) cs
+(f >< a) d = C (SumOfProd [ta:p | shallow, p <- ps]) cs
   where
     C (SumOfProd ps) cfs = f d
     C ta cas = a (d-1)
-    cs = [\(x:xs) -> cf xs (conv cas x) | d > 0, cf <- cfs]
+    cs = [\(x:xs) -> cf xs (conv cas x) | shallow, cf <- cfs]
+    shallow = d > 0 && nonEmpty ta
 
+nonEmpty :: Type -> Bool
+nonEmpty (SumOfProd ps) = not (null ps)
+
 (\/) :: Series a -> Series a -> Series a
 (a \/ b) d = C (SumOfProd (ssa ++ ssb)) (ca ++ cb)
   where
@@ -193,11 +203,9 @@
         unknown p = sumMapM ref 1 (refineList xs p)
 
         report =
-          do putStr "Counter example found"
-             case [ys | ys <- mapM total xs] of
-               [] -> putStrLn ", but too deep to fully instantiate"
-               as:_ -> do putStrLn ":"
-                          mapM_ putStrLn $ zipWith ($) (showArgs r) as
+          do putStrLn "Counter example found:"
+             mapM_ putStrLn $ zipWith ($) (showArgs r)
+                            $ head [ys | ys <- mapM total xs]
              exitWith ExitSuccess
 
 sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int
@@ -206,28 +214,35 @@
 
 -- Properties with parallel conjunction (Lindblad TFP'07)
 
-data Prop = Bool Bool | Neg Prop | And Prop Prop | ParAnd Prop Prop
+data Property =
+    Bool Bool
+  | Neg Property
+  | And Property Property
+  | ParAnd Property Property
+  | Eq Property Property
 
-eval :: Prop -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
+eval :: Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
 eval p k u = answer p (\p -> eval' p k u) u
 
 eval' (Bool b) k u = answer b k u
 eval' (Neg p) k u = eval p (k . not) u
-eval' (And p q) k u = eval p (\b -> if b then eval q k u else k b) u
-eval' (ParAnd p q) k u = eval p (\b -> if b then eval q k u else k b) unknown
+eval' (And p q) k u = eval p (\b-> if b then eval q k u else k b) u
+eval' (Eq p q) k u = eval p (\b-> if b then eval q k u else eval (Neg q) k u) u
+eval' (ParAnd p q) k u = eval p (\b-> if b then eval q k u else k b) unknown
   where
-    unknown pos = eval q (\b -> if b then u pos else k b) (\_ -> u pos)
+    unknown pos = eval q (\b-> if b then u pos else k b) (\_-> u pos)
 
-lift :: Bool -> Prop
+lift :: Bool -> Property
 lift b = Bool b
 
-neg :: Prop -> Prop
+neg :: Property -> Property
 neg p = Neg p
 
-(*&*), (*|*), (*=>*) :: Prop -> Prop -> Prop
+(*&*), (*|*), (*=>*) :: Property -> Property -> Property
 p *&* q = ParAnd p q
 p *|* q = neg (neg p *&* neg q)
 p *=>* q = neg (p *&* neg q)
+p *=* q = Eq p q
 
 -- Boolean implication
 
@@ -240,21 +255,21 @@
 data Result =
   Result { args     :: [Term]
          , showArgs :: [Term -> String]
-         , apply    :: [Term] -> Prop
+         , apply    :: [Term] -> Property
          }
 
-data Property = P (Int -> Int -> Result)
+data P = P (Int -> Int -> Result)
 
 run :: Testable a => ([Term] -> a) -> Int -> Int -> Result
 run a = f where P f = property a
 
 class Testable a where
-  property :: ([Term] -> a) -> Property
+  property :: ([Term] -> a) -> P
 
 instance Testable Bool where
   property apply = P $ \n d -> Result [] [] (Bool . apply . reverse)
 
-instance Testable Prop where
+instance Testable Property where
   property apply = P $ \n d -> Result [] [] (apply . reverse)
 
 instance (Show a, Serial a, Testable b) => Testable (a -> b) where
@@ -270,6 +285,9 @@
 depthCheck d p =
   do n <- refute $ run (const p) 0 d
      putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d
+
+smallCheck :: Testable a => Int -> a -> IO ()
+smallCheck d p = mapM_ (`depthCheck` p) [0..d]
 
 test :: Testable a => a -> IO ()
 test p = mapM_ (`depthCheck` p) [0..]
diff --git a/examples/Mate.hs b/examples/Mate.hs
--- a/examples/Mate.hs
+++ b/examples/Mate.hs
@@ -1,6 +1,6 @@
 module Mate where
 
-import LazySmallCheck
+import Test.LazySmallCheck
 import List
 
 data Kind = King | Queen | Rook | Bishop | Knight | Pawn
diff --git a/examples/test/make.sh b/examples/test/make.sh
new file mode 100644
--- /dev/null
+++ b/examples/test/make.sh
@@ -0,0 +1,15 @@
+ghc --make -O2 -i../ -i../../ TestCatch.hs
+ghc --make -O2 -i../ -i../../ TestCountdown1.hs
+ghc --make -O2 -i../ -i../../ TestCountdown2.hs
+ghc --make -O2 -i../ -i../../ TestHuffman1.hs
+ghc --make -O2 -i../ -i../../ TestHuffman2.hs
+ghc --make -O2 -i../ -i../../ TestListSet1.hs
+ghc --make -O2 -i../ -i../../ TestMate.hs
+ghc --make -O2 -i../ -i../../ TestMux1.hs
+ghc --make -O2 -i../ -i../../ TestMux2.hs
+ghc --make -O2 -i../ -i../../ TestMux3.hs
+ghc --make -O2 -i../ -i../../ TestRedBlack.hs
+ghc --make -O2 -i../ -i../../ TestRegExp.hs
+ghc --make -O2 -i../ -i../../ TestSad.hs
+ghc --make -O2 -i../ -i../../ TestSumPuz.hs
+ghc --make -O2 -i../ -i../../ TestTurner.hs
diff --git a/lazysmallcheck.cabal b/lazysmallcheck.cabal
--- a/lazysmallcheck.cabal
+++ b/lazysmallcheck.cabal
@@ -1,5 +1,5 @@
 Name:               lazysmallcheck
-Version:            0.2
+Version:            0.3
 Maintainer:         Matthew Naylor <mfn@cs.york.ac.uk>
 Homepage:           http://www.cs.york.ac.uk/~mfn/lazysmallcheck/
 Build-Depends:      base, haskell98
@@ -45,6 +45,7 @@
   examples/test/TestMate.hs
   examples/test/TestTurner.hs
   examples/test/TestMux1.hs
+  examples/test/make.sh
 
 Exposed-modules:
   Test.LazySmallCheck