diff --git a/examples/HugeLists.hs b/examples/HugeLists.hs
--- a/examples/HugeLists.hs
+++ b/examples/HugeLists.hs
@@ -1,7 +1,7 @@
 -- A stress test using lots and lots of list functions.
 {-# LANGUAGE ScopedTypeVariables, ConstraintKinds, RankNTypes, ConstraintKinds, FlexibleContexts #-}
 import QuickSpec
-import QuickSpec.Utils
+import QuickSpec.Internal.Utils
 import Data.List
 import Control.Monad
 
diff --git a/examples/IntSet.hs b/examples/IntSet.hs
--- a/examples/IntSet.hs
+++ b/examples/IntSet.hs
@@ -6,6 +6,7 @@
 
 main = quickSpec [
   monoType (Proxy :: Proxy IntSet),
+  withMaxTests 10000,
 
   series [sig1, sig2, sig3]]
   where
diff --git a/quickspec.cabal b/quickspec.cabal
--- a/quickspec.cabal
+++ b/quickspec.cabal
@@ -1,6 +1,6 @@
 Name:                quickspec
-Version:             2.1.2
-Cabal-version:       >= 1.6
+Version:             2.1.3
+Cabal-version:       >= 1.10
 Build-type:          Simple
 
 Homepage:            https://github.com/nick8325/quickspec
@@ -71,6 +71,7 @@
   branch:   master
 
 library
+  default-language: Haskell2010
   ghc-options: -W
   hs-source-dirs: src
   Exposed-modules:
@@ -111,5 +112,5 @@
     spoon,
     template-haskell,
     transformers,
-    twee-lib == 2.1.5,
+    twee-lib == 2.2,
     uglymemo
diff --git a/src/QuickSpec.hs b/src/QuickSpec.hs
--- a/src/QuickSpec.hs
+++ b/src/QuickSpec.hs
@@ -74,7 +74,12 @@
   A, B, C, D, E,
 
   -- * Declaring types
-  monoType, monoTypeObserve, vars, monoTypeWithVars, inst, Observe(..),
+  monoType, monoTypeObserve, Observe(..), inst,
+  vars, monoTypeWithVars, monoTypeObserveWithVars,
+  variableUse, VariableUse(..),
+  
+  -- * Declaring types: @TypeApplication@-friendly variants
+  mono, monoObserve, monoVars, monoObserveVars,
 
   -- * Standard signatures
   -- | The \"prelude\": a standard signature containing useful functions
@@ -90,14 +95,18 @@
   -- * Customising QuickSpec
   withMaxTermSize, withMaxTests, withMaxTestSize, defaultTo,
   withPruningDepth, withPruningTermSize, withFixedSeed,
-  withInferInstanceTypes,
+  withInferInstanceTypes, withPrintStyle, PrintStyle(..),
 
+  -- * Integrating with QuickCheck
+  (=~=),
+
   -- * Re-exported functionality
   Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary) where
 
 import QuickSpec.Internal
-import QuickSpec.Internal.Haskell(Observe(..))
+import QuickSpec.Internal.Haskell(Observe(..), PrintStyle(..), (=~=))
 import QuickSpec.Internal.Type(A, B, C, D, E)
+import QuickSpec.Internal.Explore.Schemas(VariableUse(..))
 import Data.Typeable
 import Data.Constraint
 import Test.QuickCheck
diff --git a/src/QuickSpec/Internal.hs b/src/QuickSpec/Internal.hs
--- a/src/QuickSpec/Internal.hs
+++ b/src/QuickSpec/Internal.hs
@@ -8,15 +8,17 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
 module QuickSpec.Internal where
 
-import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..))
+import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), Use(..))
 import qualified QuickSpec.Internal.Haskell as Haskell
 import qualified QuickSpec.Internal.Haskell.Resolve as Haskell
 import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck
 import qualified QuickSpec.Internal.Pruning.UntypedTwee as Twee
 import QuickSpec.Internal.Prop
 import QuickSpec.Internal.Term(Term)
+import QuickSpec.Internal.Explore.Schemas(VariableUse(..))
 import Test.QuickCheck
 import Test.QuickCheck.Random
 import Data.Constraint
@@ -156,6 +158,16 @@
     inst (Sub Dict :: () :- Ord a),
     inst (Sub Dict :: () :- Arbitrary a)]
 
+-- | Like 'monoType', but designed to be used with TypeApplications directly.
+--
+-- For example, you can add 'Foo' to your signature via:
+--
+-- @
+-- `mono` @Foo
+-- @
+mono :: forall a. (Ord a, Arbitrary a, Typeable a) => Sig
+mono = monoType (Proxy @a)
+
 -- | Declare a new monomorphic type using observational equivalence.
 -- The type must implement `Observe` and `Arbitrary`.
 monoTypeObserve :: forall proxy test outcome a.
@@ -166,16 +178,63 @@
     inst (Sub Dict :: () :- Observe test outcome a),
     inst (Sub Dict :: () :- Arbitrary a)]
 
+-- | Like 'monoTypeObserve', but designed to be used with TypeApplications directly.
+--
+-- For example, you can add 'Foo' to your signature via:
+--
+-- @
+-- `monoObserve` @Foo
+-- @
+monoObserve :: forall a test outcome.
+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
+  Sig
+monoObserve = monoTypeObserve (Proxy @a)
+
+-- | Declare a new monomorphic type using observational equivalence, saying how you want variables of that type to be named.
+monoTypeObserveWithVars :: forall proxy test outcome a.
+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
+  [String] -> proxy a -> Sig
+monoTypeObserveWithVars xs proxy =
+  monoTypeObserve proxy `mappend` vars xs proxy
+
+-- | Like 'monoTypeObserveWithVars', but designed to be used with TypeApplications directly.
+--
+-- For example, you can add 'Foo' to your signature via:
+--
+-- @
+-- `monoObserveVars` @Foo ["foo"]
+-- @
+monoObserveVars :: forall a test outcome.
+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
+  [String] -> Sig
+monoObserveVars xs = monoTypeObserveWithVars xs (Proxy @a)
+
 -- | Declare a new monomorphic type, saying how you want variables of that type to be named.
 monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig
 monoTypeWithVars xs proxy =
   monoType proxy `mappend` vars xs proxy
 
+-- | Like 'monoTypeWithVars' designed to be used with TypeApplications directly.
+--
+-- For example, you can add 'Foo' to your signature via:
+--
+-- @
+-- `monoVars` @Foo ["foo"]
+-- @
+monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig
+monoVars xs = monoTypeWithVars xs (Proxy @a)
+
 -- | Customize how variables of a particular type are named.
 vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig
 vars xs _ = instFun (Names xs :: Names a)
 
+-- | Constrain how variables of a particular type may occur in a term.
+-- The default value is @'UpTo' 4@.
+variableUse :: forall proxy a. Typeable a => VariableUse -> proxy a -> Sig
+variableUse x _ = instFun (Use x :: Use a)
+
 -- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and
+-- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and
 -- `Arbitrary` instance for each type you want it to test.
 --
 -- For example, if you are testing @`Data.Map.Map` k v@, you will need to add
@@ -235,7 +294,7 @@
 --
 -- Here is an example which first tests @0@ and @+@ and then adds @++@ and @length@:
 --
--- > main = quickSpec [sig1, sig2]
+-- > main = quickSpec (series [sig1, sig2])
 -- >   where
 -- >     sig1 = [
 -- >       con "0" (0 :: Int),
@@ -271,6 +330,13 @@
 -- | Set which type polymorphic terms are tested at.
 defaultTo :: Typeable a => proxy a -> Sig
 defaultTo proxy = Sig (\_ -> setL Haskell.lens_default_to (typeRep proxy))
+
+-- | Set how QuickSpec should display its discovered equations (default: 'ForHumans').
+--
+-- If you'd instead like to turn QuickSpec's output into QuickCheck tests, set
+-- this to 'ForQuickCheck'.
+withPrintStyle :: Haskell.PrintStyle -> Sig
+withPrintStyle style = Sig (\_ -> setL Haskell.lens_print_style style)
 
 -- | Set how hard QuickSpec tries to filter out redundant equations (default: no limit).
 --
diff --git a/src/QuickSpec/Internal/Explore.hs b/src/QuickSpec/Internal/Explore.hs
--- a/src/QuickSpec/Internal/Explore.hs
+++ b/src/QuickSpec/Internal/Explore.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
 module QuickSpec.Internal.Explore where
 
 import QuickSpec.Internal.Explore.Polymorphic
@@ -15,6 +15,7 @@
 import Control.Monad.Trans.State.Strict
 import Text.Printf
 import Data.Semigroup(Semigroup(..))
+import Data.List
 
 newtype Enumerator a = Enumerator { enumerate :: Int -> [[a]] -> [a] }
 
@@ -62,10 +63,10 @@
   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>
   (Prop (Term fun) -> m ()) ->
   (Term fun -> testcase -> result) ->
-  Int -> Int -> (Type -> Bool) -> Universe -> Enumerator (Term fun) -> m ()
-quickSpec present eval maxSize maxCommutativeSize singleUse univ enum = do
+  Int -> Int -> (Type -> VariableUse) -> Universe -> Enumerator (Term fun) -> m ()
+quickSpec present eval maxSize maxCommutativeSize use univ enum = do
   let
-    state0 = initialState singleUse univ (\t -> size t <= maxCommutativeSize) eval
+    state0 = initialState use univ (\t -> size t <= maxCommutativeSize) eval
 
     loop m n _ | m > n = return ()
     loop m n tss = do
@@ -87,6 +88,11 @@
 
   evalStateT (loop 0 maxSize (repeat [])) state0
 
+----------------------------------------------------------------------
+-- Functions that are not really to do with theory exploration,
+-- but are useful for printing the output nicely.
+----------------------------------------------------------------------
+
 pPrintSignature :: (Pretty a, Typed a) => [a] -> Doc
 pPrintSignature funs =
   text "== Functions ==" $$
@@ -97,3 +103,40 @@
     pad xs = nest (maxWidth - length xs) (text xs)
     pPrintDecl (name, ty) =
       pad name <+> text "::" <+> ty
+
+-- Put an equation that defines the function f into the form f lhs = rhs.
+-- An equation defines f if:
+--   * it is of the form f lhs = rhs (or vice versa).
+--   * f is not a background function.
+--   * lhs only contains background functions.
+--   * rhs does not contain f.
+--   * all vars in rhs appear in lhs
+prettyDefinition :: Eq fun => [fun] -> Prop (Term fun) -> Prop (Term fun)
+prettyDefinition cons (lhs :=>: t :=: u)
+  | Just (f, ts) <- defines u,
+    f `notElem` funs t,
+    null (usort (vars t) \\ vars ts) =
+    lhs :=>: u :=: t
+    -- In the case where t defines f, the equation is already oriented correctly
+  | otherwise = lhs :=>: t :=: u
+  where
+    defines (Fun f :@: ts)
+      | f `elem` cons,
+        all (`notElem` cons) (funs ts) = Just (f, ts)
+    defines _ = Nothing
+
+-- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative
+prettyAC :: (Eq f, Eq norm) => (Term f -> norm) -> Prop (Term f) -> Prop (Term f)
+prettyAC norm (lhs :=>: Fun f :@: [Var x, Fun f1 :@: [Var y, Var z]] :=: Fun f2 :@: [Var y1, Fun f3 :@: [Var x1, Var z1]])
+  | f == f1, f1 == f2, f2 == f3,
+    x == x1, y == y1, z == z1,
+    x /= y, y /= z, x /= z,
+    norm (Fun f :@: [Var x, Var y]) == norm (Fun f :@: [Var y, Var x]) =
+      lhs :=>: Fun f :@: [Fun f :@: [Var x, Var y], Var z] :=: Fun f :@: [Var x, Fun f :@: [Var y, Var z]]
+prettyAC _ prop = prop
+
+-- Add a type signature when printing the equation x = y.
+disambiguatePropType :: Prop (Term fun) -> Doc
+disambiguatePropType (_ :=>: (Var x) :=: Var _) =
+  text "::" <+> pPrintType (typ x)
+disambiguatePropType _ = pPrintEmpty
diff --git a/src/QuickSpec/Internal/Explore/Conditionals.hs b/src/QuickSpec/Internal/Explore/Conditionals.hs
--- a/src/QuickSpec/Internal/Explore/Conditionals.hs
+++ b/src/QuickSpec/Internal/Explore/Conditionals.hs
@@ -19,7 +19,7 @@
 import QuickSpec.Internal.Testing
 import QuickSpec.Internal.Terminal
 import QuickSpec.Internal.Utils
-import QuickSpec.Internal.Explore.Polymorphic
+import QuickSpec.Internal.Explore.Polymorphic hiding (Normal)
 import qualified Twee.Base as Twee
 import Data.List
 import Control.Monad
@@ -37,10 +37,9 @@
     return (norm . fmap Normal)
   add prop = do
     redundant <- conditionallyRedundant prop
-    if redundant then return False else do
-      res <- lift (add (mapFun Normal prop))
-      when res (considerConditionalising prop)
-      return res
+    unless redundant $ do
+      lift (add (mapFun Normal prop))
+      considerConditionalising prop
 
 conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe
 conditionalsUniverse tys funs =
@@ -76,10 +75,6 @@
   size Constructor{} = 0
   size (Normal f) = size f
 
-instance Arity fun => Arity (WithConstructor fun) where
-  arity Constructor{} = 1
-  arity (Normal f) = arity f
-
 instance Pretty fun => Pretty (WithConstructor fun) where
   pPrintPrec l p (Constructor f _) = pPrintPrec l p f <#> text "_con"
   pPrintPrec l p (Normal f) = pPrintPrec l p f
@@ -87,10 +82,6 @@
 instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where
   termStyle (Constructor _ _) = curried
   termStyle (Normal f) = termStyle f
-
-instance PrettyArity fun => PrettyArity (WithConstructor fun) where
-  prettyArity (Constructor _ _) = 1
-  prettyArity (Normal f) = prettyArity f
 
 instance (Predicate fun, Background fun) => Background (WithConstructor fun) where
   background (Normal f) = map (mapFun Normal) (background f)
diff --git a/src/QuickSpec/Internal/Explore/Polymorphic.hs b/src/QuickSpec/Internal/Explore/Polymorphic.hs
--- a/src/QuickSpec/Internal/Explore/Polymorphic.hs
+++ b/src/QuickSpec/Internal/Explore/Polymorphic.hs
@@ -9,10 +9,14 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RecordWildCards #-}
-module QuickSpec.Internal.Explore.Polymorphic(module QuickSpec.Internal.Explore.Polymorphic, Result(..), Universe(..)) where
+module QuickSpec.Internal.Explore.Polymorphic(
+  module QuickSpec.Internal.Explore.Polymorphic,
+  Result(..),
+  Universe(..),
+  VariableUse(..)) where
 
 import qualified QuickSpec.Internal.Explore.Schemas as Schemas
-import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..))
+import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..), VariableUse(..))
 import QuickSpec.Internal.Term
 import QuickSpec.Internal.Type
 import QuickSpec.Internal.Testing
@@ -53,14 +57,14 @@
 univ = lens pm_universe (\x y -> y { pm_universe = x })
 
 initialState ::
-  (Type -> Bool) ->
+  (Type -> VariableUse) ->
   Universe ->
   (Term fun -> Bool) ->
   (Term fun -> testcase -> result) ->
   Polymorphic testcase result fun norm
-initialState singleUse univ inst eval =
+initialState use univ inst eval =
   Polymorphic {
-    pm_schemas = Schemas.initialState singleUse (inst . fmap fun_specialised) (eval . fmap fun_specialised),
+    pm_schemas = Schemas.initialState use (inst . fmap fun_specialised) (eval . fmap fun_specialised),
     pm_universe = univ }
 
 polyFun :: Typed fun => fun -> PolyFun fun
@@ -75,7 +79,7 @@
   typeSubst_ _ x = x -- because it's supposed to be monomorphic
 
 newtype PolyM testcase result fun norm m a = PolyM { unPolyM :: StateT (Polymorphic testcase result fun norm) m a }
-  deriving (Functor, Applicative, Monad)
+  deriving (Functor, Applicative, Monad, MonadTerminal)
 
 explore ::
   (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun),
@@ -121,7 +125,7 @@
   add prop = PolyM $ do
     univ <- access univ
     let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))
-    or <$> mapM add insts
+    mapM_ add insts
 
 instance MonadTester testcase (Term fun) m =>
   MonadTester testcase (Term (PolyFun fun)) (PolyM testcase result fun norm m) where
@@ -219,13 +223,17 @@
             ho <- arrows fun,
             sub <- typeInstancesList univBase (components fun) ]
   
-    -- Add antiunifiers of all pairs of types, so that each equation
-    -- has a most general type
-    univ = usort $ oneTypeVar $ fixpoint antiunifiers univHo
+    -- Now close the type universe under "anti-substitution":
+    -- if u = typeSubst sub t, and u is in the universe, then
+    -- oneTypeVar t should be in the universe.
+    -- In practice this means replacing arbitrary subterms of
+    -- each type with a type variable.
+    univ = fixpoint (usort . oneTypeVar . concatMap antisubst) univHo
       where
-        antiunifiers tys =
-          usort $ map (unPoly . poly) $
-            tys ++ [antiunify ty1 ty2 | ty1 <- tys, ty2 <- tys]
+        antisubst ty =
+          ty:
+          [ Twee.build (Twee.replacePosition n (Twee.var (Twee.V 0)) (Twee.singleton ty))
+          | n <- [0..Twee.len ty-1] ]
 
     components ty =
       case unpackArrow ty of
diff --git a/src/QuickSpec/Internal/Explore/Schemas.hs b/src/QuickSpec/Internal/Explore/Schemas.hs
--- a/src/QuickSpec/Internal/Explore/Schemas.hs
+++ b/src/QuickSpec/Internal/Explore/Schemas.hs
@@ -11,6 +11,7 @@
 import QuickSpec.Internal.Type
 import QuickSpec.Internal.Testing
 import QuickSpec.Internal.Utils
+import QuickSpec.Internal.Terminal
 import qualified QuickSpec.Internal.Explore.Terms as Terms
 import QuickSpec.Internal.Explore.Terms(Terms)
 import Control.Monad.Trans.State.Strict hiding (State)
@@ -23,9 +24,16 @@
 import Control.Monad
 import Twee.Label
 
+-- | Constrains how variables of a particular type may occur in a term.
+data VariableUse =
+    UpTo Int -- ^ @UpTo n@: terms may contain up to @n@ distinct variables of this type
+             -- (in some cases, laws with more variables may still be found)
+  | Linear   -- ^ Each variable in the term must be distinct
+  deriving (Eq, Show)
+
 data Schemas testcase result fun norm =
   Schemas {
-    sc_single_use :: Type -> Bool,
+    sc_use :: Type -> VariableUse,
     sc_instantiate_singleton :: Term fun -> Bool,
     sc_empty :: Terms testcase result (Term fun) norm,
     sc_classes :: Terms testcase result (Term fun) norm,
@@ -33,7 +41,7 @@
     sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm) }
 
 classes = lens sc_classes (\x y -> y { sc_classes = x })
-single_use = lens sc_single_use (\x y -> y { sc_single_use = x })
+use = lens sc_use (\x y -> y { sc_use = x })
 instances = lens sc_instances (\x y -> y { sc_instances = x })
 instantiated = lens sc_instantiated (\x y -> y { sc_instantiated = x })
 
@@ -41,13 +49,13 @@
 instance_ t = reading (\Schemas{..} -> keyDefault t sc_empty # instances)
 
 initialState ::
-  (Type -> Bool) ->
+  (Type -> VariableUse) ->
   (Term fun -> Bool) ->
   (Term fun -> testcase -> result) ->
   Schemas testcase result fun norm
-initialState singleUse inst eval =
+initialState use inst eval =
   Schemas {
-    sc_single_use = singleUse,
+    sc_use = use,
     sc_instantiate_singleton = inst,
     sc_empty = Terms.initialState eval,
     sc_classes = Terms.initialState eval,
@@ -61,37 +69,38 @@
 -- The schema is represented as a term where there is only one distinct variable of each type
 explore ::
   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,
-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>
+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>
   Term fun -> StateT (Schemas testcase result fun norm) m (Result fun)
 explore t0 = do
-  let t = mostSpecific t0
-  res <- zoom classes (Terms.explore t)
-  singleUse <- access single_use
-  case res of
-    Terms.Singleton -> do
-      inst <- gets sc_instantiate_singleton
-      if inst t then
-        instantiateRep t
-       else do
-        -- Add the most general instance of the schema
-        zoom (instance_ t) (Terms.explore (mostGeneral singleUse t0))
-        return (Accepted [])
-    Terms.Discovered ([] :=>: _ :=: u) ->
-      exploreIn u t
-    Terms.Knew ([] :=>: _ :=: u) ->
-      exploreIn u t
-    _ -> error "term layer returned non-equational property"
+  use <- access use
+  if or [use ty == UpTo 0 | ty <- usort (map typ (vars t0))] then return (Rejected []) else do
+    let t = mostSpecific t0
+    res <- zoom classes (Terms.explore t)
+    case res of
+      Terms.Singleton -> do
+        inst <- gets sc_instantiate_singleton
+        if inst t then
+          instantiateRep t
+         else do
+          -- Add the most general instance of the schema
+          zoom (instance_ t) (Terms.explore (mostGeneral use t0))
+          return (Accepted [])
+      Terms.Discovered ([] :=>: _ :=: u) ->
+        exploreIn u t
+      Terms.Knew ([] :=>: _ :=: u) ->
+        exploreIn u t
+      _ -> error "term layer returned non-equational property"
 
 {-# INLINEABLE exploreIn #-}
 exploreIn ::
   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,
-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>
+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>
   Term fun -> Term fun ->
   StateT (Schemas testcase result fun norm) m (Result fun)
 exploreIn rep t = do
   -- First check if schema is redundant
-  singleUse <- access single_use
-  res <- zoom (instance_ rep) (Terms.explore (mostGeneral singleUse t))
+  use <- access use
+  res <- zoom (instance_ rep) (Terms.explore (mostGeneral use t))
   case res of
     Terms.Discovered prop -> do
       add prop
@@ -111,7 +120,7 @@
 {-# INLINEABLE instantiateRep #-}
 instantiateRep ::
   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,
-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>
+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>
   Term fun ->
   StateT (Schemas testcase result fun norm) m (Result fun)
 instantiateRep t = do
@@ -121,13 +130,13 @@
 {-# INLINEABLE instantiate #-}
 instantiate ::
   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,
-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>
+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>
   Term fun -> Term fun ->
   StateT (Schemas testcase result fun norm) m (Result fun)
 instantiate rep t = do
-  singleUse <- access single_use
+  use <- access use
   zoom (instance_ rep) $ do
-    let instances = sortBy (comparing generality) (allUnifications singleUse (mostGeneral singleUse t))
+    let instances = sortBy (comparing generality) (allUnifications use (mostGeneral use t))
     Accepted <$> catMaybes <$> forM instances (\t -> do
       res <- Terms.explore t
       case res of
@@ -140,30 +149,46 @@
 generality :: Term f -> (Int, [Var])
 generality t = (-length (usort (vars t)), vars t)
 
+mkVar :: Type -> Int -> Var
+mkVar ty n = V ty m
+  -- Try to make sure that variables of different types don't end up with the
+  -- same number. It would be better to deal with this in QuickSpec.Term.
+  -- (Note: the problem we are trying to avoid is that, if two variables have
+  -- the same number and different but unifiable types, then a type substitution
+  -- can turn them into the same variable.)
+  where
+    m = fromIntegral (labelNum (label (ty, n)))
+
 -- | Instantiate a schema by making all the variables different.
-mostGeneral :: (Type -> Bool) -> Term f -> Term f
-mostGeneral singleUse s = evalState (aux s) Map.empty
+mostGeneral :: (Type -> VariableUse) -> Term f -> Term f
+mostGeneral use s = evalState (aux s) Map.empty
   where
     aux (Var (V ty _)) = do
       m <- get
       let n :: Int
           n = Map.findWithDefault 0 ty m
-      unless (singleUse ty) $
+      unless (use ty == UpTo 1) $
         put $! Map.insert ty (n+1) m
-      let m = fromIntegral (labelNum (label (ty, n)))
-      return (Var (V ty m))
+      return (Var (mkVar ty n))
     aux (Fun f) = return (Fun f)
     aux (t :$: u) = liftM2 (:$:) (aux t) (aux u)
 
 mostSpecific :: Term f -> Term f
-mostSpecific = subst (\(V ty _) -> Var (V ty 0))
+mostSpecific = subst (\(V ty _) -> Var (mkVar ty 0))
 
-allUnifications :: (Type -> Bool) -> Term fun -> [Term fun]
-allUnifications singleUse t = map f ss
+allUnifications :: (Type -> VariableUse) -> Term fun -> [Term fun]
+allUnifications use t =
+  [ subst (\x -> Var (Map.findWithDefault undefined x s)) t | s <- ss ]
   where
-    vs = [ map (x,) (select xs) | xs <- partitionBy typ (usort (vars t)), x <- xs ]
-    ss = map Map.fromList (sequence vs)
-    go s x = Map.findWithDefault undefined x s
-    f s = subst (Var . go s) t
-    select [V ty x] | not (singleUse ty) = [V ty x, V ty (succ x)]
-    select xs = take 4 xs
+    ss =
+      map Map.fromList $ map concat $ sequence
+        [substsFor xs (typ y) | xs@(y:_) <- partitionBy typ (usort (vars t))]
+
+    substsFor xs ty =
+      case use ty of
+        UpTo k ->
+          sequence [[(x, v) | v <- take k vs] | x <- xs]
+        Linear ->
+          map (zip xs) (permutations (take (length xs) vs))
+      where
+        vs = map (mkVar ty) [0..]
diff --git a/src/QuickSpec/Internal/Explore/Terms.hs b/src/QuickSpec/Internal/Explore/Terms.hs
--- a/src/QuickSpec/Internal/Explore/Terms.hs
+++ b/src/QuickSpec/Internal/Explore/Terms.hs
@@ -14,6 +14,7 @@
 import Control.Monad.Trans.State.Strict hiding (State)
 import Data.Lens.Light
 import QuickSpec.Internal.Utils
+import QuickSpec.Internal.Terminal
 
 data Terms testcase result term norm =
   Terms {
@@ -56,14 +57,14 @@
 -- The representatives of the equivalence classes are guaranteed not to change.
 --
 -- Discovered properties are not added to the pruner.
-explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>
+explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m, MonadTerminal m) =>
   term -> StateT (Terms testcase result term norm) m (Result term)
 explore t = do
   res <- explore' t
-  -- case res of
-  --   Discovered prop -> traceM ("discovered " ++ prettyShow prop)
-  --   Knew prop -> traceM ("knew " ++ prettyShow prop)
-  --   Singleton -> traceM ("singleton " ++ prettyShow t)
+  --case res of
+  --  Discovered prop -> putLine ("discovered " ++ prettyShow prop)
+  --  Knew prop -> putLine ("knew " ++ prettyShow prop)
+  --  Singleton -> putLine ("singleton " ++ prettyShow t)
   return res
 explore' :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>
   term -> StateT (Terms testcase result term norm) m (Result term)
diff --git a/src/QuickSpec/Internal/Haskell.hs b/src/QuickSpec/Internal/Haskell.hs
--- a/src/QuickSpec/Internal/Haskell.hs
+++ b/src/QuickSpec/Internal/Haskell.hs
@@ -22,7 +22,6 @@
 import QuickSpec.Internal.Pruning
 import Test.QuickCheck hiding (total, classify, subterms, Fun)
 import Data.Constraint hiding ((\\))
-import Data.List
 import Data.Proxy
 import qualified Twee.Base as Twee
 import QuickSpec.Internal.Term
@@ -36,7 +35,7 @@
 import qualified QuickSpec.Internal.Pruning.Twee as Twee
 import QuickSpec.Internal.Explore hiding (quickSpec)
 import qualified QuickSpec.Internal.Explore
-import QuickSpec.Internal.Explore.Polymorphic(Universe(..))
+import QuickSpec.Internal.Explore.Polymorphic(Universe(..), VariableUse(..))
 import QuickSpec.Internal.Pruning.Background(Background)
 import Control.Monad
 import Control.Monad.Trans.State.Strict
@@ -45,7 +44,7 @@
 import QuickSpec.Internal.Utils
 import Data.Lens.Light
 import GHC.TypeLits
-import QuickSpec.Internal.Explore.Conditionals
+import QuickSpec.Internal.Explore.Conditionals hiding (Normal)
 import Control.Spoon
 import qualified Data.Set as Set
 import qualified Test.QuickCheck.Poly as Poly
@@ -76,6 +75,8 @@
     inst (Names ["f", "g", "h"] :: Names (A -> B)),
     inst (Names ["dict"] :: Names (Dict ClassA)),
     inst (Names ["x", "y", "z", "w"] :: Names A),
+    -- Allow up to 4 variables per type by default
+    inst (Use (UpTo 4) :: Use A),
     -- Standard instances
     baseType (Proxy :: Proxy ()),
     baseType (Proxy :: Proxy Int),
@@ -125,6 +126,7 @@
     -- From Arbitrary to Gen
     inst $ \(Dict :: Dict (Arbitrary A)) -> arbitrary :: Gen A,
     -- Observation functions
+    inst $ \(Dict :: Dict (Ord A)) -> OrdInstance :: OrdInstance A,
     inst (\(Dict :: Dict (Observe A B C)) -> observeObs :: ObserveData C B),
     inst (\(Dict :: Dict (Ord A)) -> observeOrd :: ObserveData A A),
     inst (\(Dict :: Dict (Arbitrary A)) (obs :: ObserveData B C) -> observeFunction obs :: ObserveData (A -> B) C),
@@ -134,10 +136,13 @@
     -- Needed for typeclass-polymorphic predicates to work currently
     inst (\(Dict :: Dict ClassA) -> Dict :: Dict (Arbitrary (Dict ClassA)))]
 
+data OrdInstance a where
+  OrdInstance :: Ord a => OrdInstance a
+
 -- A token used in the instance list for types that shouldn't generate warnings
 data NoWarnings a = NoWarnings
 
-data SingleUse a = SingleUse
+data Use a = Use VariableUse
 
 instance c => Arbitrary (Dict c) where
   arbitrary = return Dict
@@ -166,6 +171,10 @@
 instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where
   observe (x, obs) f = observe obs (f x)
 
+-- | Like 'Test.QuickCheck.===', but using the 'Observe' typeclass instead of 'Eq'.
+(=~=) :: (Show test, Show outcome, Observe test outcome a) => a -> a -> Property
+a =~= b = property $ \test -> observe test a Test.QuickCheck.=== observe test b
+
 -- An observation function along with instances.
 -- The parameters are in this order so that we can use findInstance to get at appropriate Wrappers.
 data ObserveData a outcome where
@@ -240,6 +249,9 @@
 findGenerator def insts ty =
   bringFunctor <$> (findInstance insts (defaultTo def ty) :: Maybe (Value Gen))
 
+findOrdInstance :: Instances -> Type -> Maybe (Value OrdInstance)
+findOrdInstance insts ty = findInstance insts ty
+
 findObserver :: Instances -> Type -> Maybe (Gen (Value Identity -> Value Ordy))
 findObserver insts ty = do
   inst <- findInstance insts ty :: Maybe (Value WrappedObserveData)
@@ -274,13 +286,23 @@
   Constant {
     con_name  :: String,
     con_style :: TermStyle,
-    con_pretty_arity :: Int,
     con_value :: Value Identity,
     con_type :: Type,
     con_constraints :: [Type],
     con_size :: Int,
     con_classify :: Classification Constant }
 
+makeQuickcheckFun :: String -> Constant
+makeQuickcheckFun nm = Constant
+  { con_name  = nm
+  , con_style = infixStyle 9  -- high precedence to always force parens
+  , con_value = undefined
+  , con_type = undefined
+  , con_constraints = undefined
+  , con_size = 1
+  , con_classify = Function
+  }
+
 instance Eq Constant where
   x == y =
     con_name x == con_name y && typ (con_value x) == typ (con_value y)
@@ -288,12 +310,7 @@
 instance Ord Constant where
   compare =
     comparing $ \con ->
-      (con_name con, twiddle (arity con), typ con)
-      where
-        -- This trick comes from Prover9 and improves the ordering somewhat
-        twiddle 1 = 2
-        twiddle 2 = 1
-        twiddle x = x
+      (typeArity (typ con), typ con, con_name con)
 
 instance Background Constant
 
@@ -313,11 +330,6 @@
           | isOp name && typeArity (typ val) >= 2 -> infixStyle 5
           | isOp name -> prefix
           | otherwise -> curried,
-    con_pretty_arity =
-      case () of
-        _ | isOp name && typeArity (typ val) >= 2 -> 2
-          | isOp name -> 1
-          | otherwise -> typeArity (typ val),
     con_value = val,
     con_type = ty,
     con_constraints = constraints,
@@ -372,15 +384,9 @@
 instance PrettyTerm Constant where
   termStyle = con_style
 
-instance PrettyArity Constant where
-  prettyArity = con_pretty_arity
-
 instance Sized Constant where
   size = con_size
 
-instance Arity Constant where
-  arity = typeArity . typ
-
 instance Predicate Constant where
   classify = con_classify
 
@@ -478,6 +484,12 @@
     inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)
     inst Dict = arbitrary `suchThat` uncrry pred
 
+-- | How QuickSpec should style equations.
+data PrintStyle
+  = ForHumans
+  | ForQuickCheck
+  deriving (Eq, Ord, Show, Read, Bounded, Enum)
+
 data Config =
   Config {
     cfg_quickCheck :: QuickCheck.Config,
@@ -492,7 +504,8 @@
     cfg_default_to :: Type,
     cfg_infer_instance_types :: Bool,
     cfg_background :: [Prop (Term Constant)],
-    cfg_print_filter :: Prop (Term Constant) -> Bool
+    cfg_print_filter :: Prop (Term Constant) -> Bool,
+    cfg_print_style :: PrintStyle
     }
 
 lens_quickCheck = lens cfg_quickCheck (\x y -> y { cfg_quickCheck = x })
@@ -505,6 +518,7 @@
 lens_infer_instance_types = lens cfg_infer_instance_types (\x y -> y { cfg_infer_instance_types = x })
 lens_background = lens cfg_background (\x y -> y { cfg_background = x })
 lens_print_filter = lens cfg_print_filter (\x y -> y { cfg_print_filter = x })
+lens_print_style = lens cfg_print_style (\x y -> y { cfg_print_style = x })
 
 defaultConfig :: Config
 defaultConfig =
@@ -518,7 +532,8 @@
     cfg_default_to = typeRep (Proxy :: Proxy Int),
     cfg_infer_instance_types = False,
     cfg_background = [],
-    cfg_print_filter = \_ -> True }
+    cfg_print_filter = \_ -> True,
+    cfg_print_style = ForHumans }
 
 -- Extra types for the universe that come from in-scope instances.
 instanceTypes :: Instances -> Config -> [Type]
@@ -593,55 +608,33 @@
       [true | any (/= Function) (map classify (f cfg_constants))] ++
       f cfg_constants ++ concatMap selectors (f cfg_constants)
     constants = constantsOf concat
-    
+
     univ = conditionalsUniverse (instanceTypes instances cfg) constants
     instances = cfg_instances `mappend` baseInstances
 
     eval = evalHaskell cfg_default_to instances
+    was_observed = isNothing . findOrdInstance instances  -- it was observed if there is no Ord instance directly in scope
 
     present funs prop = do
       norm <- normaliser
-      let prop' = makeDefinition funs (ac norm (conditionalise prop))
+      let prop' = prettyDefinition funs (prettyAC norm (conditionalise prop))
       when (cfg_print_filter prop) $ do
         (n :: Int, props) <- get
         put (n+1, prop':props)
         putLine $
-          printf "%3d. %s" n $ show $
-            prettyProp (names instances) prop' <+> maybeType prop
-
-    -- Put an equation that defines the function f into the form f lhs = rhs.
-    -- An equation defines f if:
-    --   * it is of the form f lhs = rhs (or vice versa).
-    --   * f is not a background function.
-    --   * lhs only contains background functions.
-    --   * rhs does not contain f.
-    --   * all vars in rhs appear in lhs
-    makeDefinition cons (lhs :=>: t :=: u)
-      | Just (f, ts) <- defines u,
-        f `notElem` funs t,
-        null (usort (vars t) \\ vars ts) =
-        lhs :=>: u :=: t
-        -- In the case where t defines f, the equation is already oriented correctly
-      | otherwise = lhs :=>: t :=: u
-      where
-        defines (Fun f :@: ts)
-          | f `elem` cons,
-            all (`notElem` cons) (funs ts) = Just (f, ts)
-        defines _ = Nothing
-
-    -- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative
-    ac norm (lhs :=>: Fun f :@: [Var x, Fun f1 :@: [Var y, Var z]] :=: Fun f2 :@: [Var y1, Fun f3 :@: [Var x1, Var z1]])
-      | f == f1, f1 == f2, f2 == f3,
-        x == x1, y == y1, z == z1,
-        x /= y, y /= z, x /= z,
-        norm (Fun f :@: [Var x, Var y]) == norm (Fun f :@: [Var y, Var x]) =
-          lhs :=>: Fun f :@: [Fun f :@: [Var x, Var y], Var z] :=: Fun f :@: [Var x, Fun f :@: [Var y, Var z]]
-    ac _ prop = prop
-
-    -- Add a type signature when printing the equation x = y.
-    maybeType (_ :=>: x@(Var _) :=: Var _) =
-      text "::" <+> pPrintType (typ x)
-    maybeType _ = pPrintEmpty
+          case cfg_print_style of
+            ForHumans ->
+              printf "%3d. %s" n $ show $
+                prettyProp (names instances) prop' <+> disambiguatePropType prop
+            ForQuickCheck ->
+              renderStyle (style {lineLength = 78}) $ nest 2 $
+                prettyPropQC
+                  was_observed
+                  makeQuickcheckFun
+                  n
+                  (names instances)
+                  prop'
+                  <+> disambiguatePropType prop
 
     -- XXX do this during testing
     constraintsOk = memo $ \con ->
@@ -659,8 +652,9 @@
 
     conditions t = usort [p | f <- funs t, Selector _ p _ <- [classify f]]
 
-    singleUse ty =
-      isJust (findInstance instances ty :: Maybe (Value SingleUse))
+    use ty =
+      ofValue (\(Use x) -> x) $ fromJust $
+      (findInstance instances ty :: Maybe (Value Use))
 
     mainOf n f g = do
       unless (null (f cfg_constants)) $ do
@@ -670,10 +664,14 @@
       when (n > 0) $ do
         putText (prettyShow (warnings univ instances cfg))
         putLine "== Laws =="
+        when (cfg_print_style == ForQuickCheck) $ do
+          putLine "quickspec_laws :: [(String, Property)]"
+          putLine "quickspec_laws ="
       let pres = if n == 0 then \_ -> return () else present (constantsOf f)
-      QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size singleUse univ
+      QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size use univ
         (enumerator (map Fun (constantsOf g)))
       when (n > 0) $ do
+        when (cfg_print_style == ForQuickCheck) $ putLine "  ]"
         putLine ""
 
     main = do
diff --git a/src/QuickSpec/Internal/Prop.hs b/src/QuickSpec/Internal/Prop.hs
--- a/src/QuickSpec/Internal/Prop.hs
+++ b/src/QuickSpec/Internal/Prop.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators #-}
 module QuickSpec.Internal.Prop where
 
+import Data.Bool (bool)
 import Control.Monad
 import qualified Data.DList as DList
 import Data.Ord
@@ -10,7 +11,6 @@
 import QuickSpec.Internal.Term
 import GHC.Generics(Generic)
 import qualified Data.Map.Strict as Map
-import qualified Data.Set as Set
 import Control.Monad.Trans.State.Strict
 import Data.List
 
@@ -83,19 +83,44 @@
 -- Making properties look pretty (naming variables, etc.)
 ----------------------------------------------------------------------
 
-class PrettyArity fun where
-  prettyArity :: fun -> Int
-  prettyArity _ = 0
-
-instance (PrettyArity fun1, PrettyArity fun2) => PrettyArity (fun1 :+: fun2) where
-  prettyArity (Inl x) = prettyArity x
-  prettyArity (Inr x) = prettyArity x
-
 prettyProp ::
-  (Typed fun, Apply (Term fun), PrettyTerm fun, PrettyArity fun) =>
+  (Typed fun, Apply (Term fun), PrettyTerm fun) =>
   (Type -> [String]) -> Prop (Term fun) -> Doc
-prettyProp cands = pPrint . nameVars cands
+prettyProp cands = pPrint . snd . nameVars cands
 
+prettyPropQC ::
+  (Typed fun, Apply (Term fun), PrettyTerm fun) =>
+  (Type -> Bool) -> (String -> fun) -> Int -> (Type -> [String]) -> Prop (Term fun) -> Doc
+prettyPropQC was_observed mk_fun nth cands x
+  = hang (text first_char <+> text "(" <+> ((text $ show $ show $ pPrint law))) 2
+  $ hang (hsep [text ",", text "property", text "$"]) 4
+  $ hang ppr_binds 4
+  $ ppr_ctx <+> (pPrint (eq_fn :$: lhs :$: rhs) <> text ")")
+
+  where
+    eq = mk_fun "==="
+    obs_eq = mk_fun "=~="
+    eq_fn = Fun $ Ordinary $ bool eq obs_eq $ was_observed $ typ lhs_for_type
+
+
+    first_char =
+      case nth of
+        1 -> "["
+        _ -> ","
+    ppr_ctx =
+      case length ctx of
+        0 -> pPrintEmpty
+        _ -> (hsep $ punctuate (text " &&") $ fmap (parens . pPrint) ctx) <+> text "==>"
+
+    (_ :=>: (lhs_for_type :=: _)) = x
+    (var_defs, law@(ctx :=>: (lhs :=: rhs))) = nameVars cands x
+    print_sig name ty = parens $ text name <+> text "::" <+> pPrintType ty
+    ppr_binds =
+      case Map.size var_defs of
+        0 -> pPrintEmpty
+        _ -> (text "\\ " <> sep (fmap (uncurry print_sig) (Map.assocs var_defs))) <+> text "->"
+
+
 data Named fun = Name String | Ordinary fun
 instance Pretty fun => Pretty (Named fun) where
   pPrintPrec _ _ (Name name) = text name
@@ -104,14 +129,16 @@
   termStyle Name{} = curried
   termStyle (Ordinary fun) = termStyle fun
 
-nameVars :: (Type -> [String]) -> Prop (Term fun) -> Prop (Term (Named fun))
+nameVars :: (Type -> [String]) -> Prop (Term fun) -> (Map.Map String Type, Prop (Term (Named fun)))
 nameVars cands p =
-  subst (\x -> Map.findWithDefault undefined x sub) (fmap (fmap Ordinary) p)
+  (var_defs, subst (\x -> Map.findWithDefault undefined x sub) (fmap (fmap Ordinary) p))
   where
-    sub = Map.fromList (evalState (mapM assign (nub (vars p))) Set.empty)
+    sub = Map.fromList sub_map
+    (sub_map, var_defs) = (runState (mapM assign (nub (vars p))) Map.empty)
     assign x = do
       s <- get
-      let names = supply (cands (typ x))
-          name = head (filter (`Set.notMember` s) names)
-      modify (Set.insert name)
+      let ty = typ x
+          names = supply (cands ty)
+          name = head (filter (`Map.notMember` s) names)
+      modify (Map.insert name ty)
       return (x, Fun (Name name))
diff --git a/src/QuickSpec/Internal/Pruning.hs b/src/QuickSpec/Internal/Pruning.hs
--- a/src/QuickSpec/Internal/Pruning.hs
+++ b/src/QuickSpec/Internal/Pruning.hs
@@ -13,12 +13,12 @@
 
 class Monad m => MonadPruner term norm m | m -> term norm where
   normaliser :: m (term -> norm)
-  add :: Prop term -> m Bool
+  add :: Prop term -> m ()
 
   default normaliser :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => m (term -> norm)
   normaliser = lift normaliser
 
-  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m Bool
+  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m ()
   add = lift . add
 
 instance MonadPruner term norm m => MonadPruner term norm (StateT s m)
@@ -37,7 +37,7 @@
 
 instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where
   normaliser = ReadOnlyPruner normaliser
-  add _ = return True
+  add _ = return ()
 
 newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a)
   deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadTester testcase term)
@@ -46,7 +46,7 @@
   normaliser = lift normaliser
   add prop = do
     res <- lift (add prop)
-    when res (WatchPruner (modify (prop:)))
+    WatchPruner (modify (prop:))
     return res
 
 watchPruner :: Monad m => WatchPruner term m a -> m (a, [Prop term])
diff --git a/src/QuickSpec/Internal/Pruning/PartialApplication.hs b/src/QuickSpec/Internal/Pruning/PartialApplication.hs
--- a/src/QuickSpec/Internal/Pruning/PartialApplication.hs
+++ b/src/QuickSpec/Internal/Pruning/PartialApplication.hs
@@ -12,6 +12,7 @@
 import QuickSpec.Internal.Testing
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
+import Twee.Base(Arity(..))
 
 data PartiallyApplied f =
     -- A partially-applied function symbol.
@@ -31,16 +32,12 @@
   arity (Apply _) = 2
 
 instance Pretty f => Pretty (PartiallyApplied f) where
-  pPrint (Partial f _) = pPrint f
+  pPrint (Partial f n) = pPrint f <#> text "@" <#> pPrint n
   pPrint (Apply _) = text "$"
 
 instance PrettyTerm f => PrettyTerm (PartiallyApplied f) where
   termStyle (Partial f _) = termStyle f
-  termStyle (Apply _) = invisible
-
-instance PrettyArity f => PrettyArity (PartiallyApplied f) where
-  prettyArity (Partial f _) = prettyArity f
-  prettyArity (Apply _) = 1
+  termStyle (Apply _) = infixStyle 2
 
 instance Typed f => Typed (PartiallyApplied f) where
   typ (Apply ty) = arrowType [ty] ty
@@ -50,10 +47,6 @@
   typeSubst_ sub (Apply ty) = Apply (typeSubst_ sub ty)
   typeSubst_ sub (Partial f n) = Partial (typeSubst_ sub f) n
 
-getTotal :: Arity f => PartiallyApplied f -> Maybe f
-getTotal (Partial f n) | arity f == n = Just f
-getTotal _ = Nothing
-
 partial :: f -> Term (PartiallyApplied f)
 partial f = Fun (Partial f 0)
 
@@ -61,8 +54,8 @@
 total f = Partial f (arity f)
 
 smartApply ::
-  (Arity f, Typed f) => Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
-smartApply (Fun (Partial f n) :@: ts) u | n < arity f =
+  Typed f => Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
+smartApply (Fun (Partial f n) :@: ts) u =
   Fun (Partial f (n+1)) :@: (ts ++ [u])
 smartApply t u = simpleApply t u
 
@@ -72,12 +65,13 @@
 simpleApply t u =
   Fun (Apply (typ t)) :@: [t, u]
 
-instance (Arity f, Typed f, Background f) => Background (PartiallyApplied f) where
+instance (Typed f, Background f) => Background (PartiallyApplied f) where
   background (Partial f _) =
-    map (mapFun (\f -> Partial f (arity f))) (background f) ++
+    map (mapFun (\f -> Partial f arity)) (background f) ++
     [ simpleApply (partial n) (vs !! n) === partial (n+1)
-    | n <- [0..arity f-1] ]
+    | n <- [0..arity-1] ]
     where
+      arity = typeArity (typ f)
       partial i =
         Fun (Partial f i) :@: take i vs
       vs = map Var (zipWith V (typeArgs (typ f)) [0..])
@@ -90,7 +84,7 @@
 instance MonadTrans (Pruner fun) where
   lift = Pruner
 
-instance (PrettyTerm fun, Typed fun, Arity fun, MonadPruner (Term (PartiallyApplied fun)) norm pruner) => MonadPruner (Term fun) norm (Pruner fun pruner) where
+instance (PrettyTerm fun, Typed fun, MonadPruner (Term (PartiallyApplied fun)) norm pruner) => MonadPruner (Term fun) norm (Pruner fun pruner) where
   normaliser =
     Pruner $ do
       norm <- normaliser
@@ -101,7 +95,7 @@
     Pruner $ do
       add (encode <$> canonicalise prop)
 
-encode :: (Typed fun, Arity fun) => Term fun -> Term (PartiallyApplied fun)
+encode :: Typed fun => Term fun -> Term (PartiallyApplied fun)
 encode (Var x) = Var x
 encode (Fun f) = partial f
 encode (t :$: u) = smartApply (encode t) (encode u)
diff --git a/src/QuickSpec/Internal/Pruning/Types.hs b/src/QuickSpec/Internal/Pruning/Types.hs
--- a/src/QuickSpec/Internal/Pruning/Types.hs
+++ b/src/QuickSpec/Internal/Pruning/Types.hs
@@ -4,8 +4,7 @@
 module QuickSpec.Internal.Pruning.Types where
 
 import QuickSpec.Internal.Pruning
-import qualified QuickSpec.Internal.Pruning.Background as Background
-import QuickSpec.Internal.Pruning.Background(Background)
+import QuickSpec.Internal.Pruning.Background(Background(..))
 import QuickSpec.Internal.Testing
 import QuickSpec.Internal.Term
 import QuickSpec.Internal.Type
@@ -14,6 +13,7 @@
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
 import qualified Twee.Base as Twee
+import Twee.Base(Arity(..))
 
 data Tagged fun =
     Func fun
@@ -66,11 +66,11 @@
 
   add prop = lift (add (encode <$> canonicalise prop))
 
-instance (Typed fun, Arity fun) => Background (Tagged fun) where
+instance (Typed fun, Twee.Arity fun, Background fun) => Background (Tagged fun) where
   background = typingAxioms
 
 -- Compute the typing axioms for a function or type tag.
-typingAxioms :: (Typed fun, Arity fun) =>
+typingAxioms :: (Typed fun, Twee.Arity fun, Background fun) =>
   Tagged fun -> [Prop (UntypedTerm fun)]
 typingAxioms (Tag ty) =
   [tag ty (tag ty x) === tag ty x]
@@ -78,7 +78,8 @@
     x = Var (V ty 0)
 typingAxioms (Func func) =
   [tag res t === t] ++
-  [tagArg i ty === t | (i, ty) <- zip [0..] args]
+  [tagArg i ty === t | (i, ty) <- zip [0..] args] ++
+  map (fmap encode) (background func)
   where
     f = Fun (Func func)
     xs = take n (map (Var . V typeVar) [0..])
diff --git a/src/QuickSpec/Internal/Pruning/UntypedTwee.hs b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
--- a/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
+++ b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
@@ -16,7 +16,7 @@
 import Twee hiding (Config(..))
 import Twee.Rule hiding (normalForms)
 import Twee.Proof hiding (Config, defaultConfig)
-import Twee.Base(Ordered(..), Extended(..), EqualsBonus)
+import Twee.Base(Ordered(..), Extended(..), Arity(..), EqualsBonus)
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State.Strict hiding (State)
 import Control.Monad.Trans.Class
@@ -77,16 +77,10 @@
   add ([] :=>: t :=: u) = Pruner $ do
     state <- lift get
     config <- ask
-    let
-      t' = normalFormsTwee state t
-      u' = normalFormsTwee state u
-    -- Add the property anyway in case it could only be joined
-    -- by considering all normal forms
     lift (put $! addTwee config t u state)
-    return (Set.null (Set.intersection t' u'))
 
   add _ =
-    return True
+    return ()
     --error "twee pruner doesn't support non-unit equalities"
 
 normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
diff --git a/src/QuickSpec/Internal/Term.hs b/src/QuickSpec/Internal/Term.hs
--- a/src/QuickSpec/Internal/Term.hs
+++ b/src/QuickSpec/Internal/Term.hs
@@ -9,12 +9,13 @@
 import QuickSpec.Internal.Utils
 import Control.Monad
 import GHC.Generics(Generic)
-import Test.QuickCheck(CoArbitrary)
+import Test.QuickCheck(CoArbitrary(..))
 import Data.DList(DList)
 import qualified Data.DList as DList
-import Twee.Base(Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)
+import Twee.Base(Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)
 import Twee.Pretty
 import qualified Data.Map.Strict as Map
+import Data.Map(Map)
 import Data.List
 import Data.Ord
 
@@ -24,13 +25,47 @@
 
 -- | A variable, which has a type and a number.
 data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }
-  deriving (Eq, Ord, Show, Generic, CoArbitrary)
+  deriving (Eq, Ord, Show, Generic)
 
+instance CoArbitrary Var where
+  coarbitrary = coarbitrary . var_id
+
 instance Typed Var where
   typ x = var_ty x
   otherTypesDL _ = mzero
   typeSubst_ sub (V ty x) = V (typeSubst_ sub ty) x
 
+match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
+match (Var x) t = Just (Map.singleton x t)
+match (Fun f) (Fun g)
+  | f == g = Just Map.empty
+  | otherwise = Nothing
+match (f :$: x) (g :$: y) = do
+  m1 <- match f g
+  m2 <- match x y
+  guard (and [t == u | (t, u) <- Map.elems (Map.intersectionWith (,) m1 m2)])
+  return (Map.union m1 m2)
+
+unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
+unify t u = loop Map.empty [(t, u)]
+  where
+    loop sub [] = Just sub
+    loop sub ((Fun f, Fun g):xs)
+      | f == g = loop sub xs
+    loop sub ((f :$: x, g :$: y):xs) =
+      loop sub ((f, g):(x, y):xs)
+    loop sub ((Var x, t):xs)
+      | t == Var x = loop sub xs
+      | x `elem` vars t = Nothing
+      | otherwise =
+        loop
+          (Map.insert x t (fmap (replace x t) sub))
+          [(replace x t u, replace x t v) | (u, v) <- xs]
+    loop sub ((t, Var x):xs) = loop sub ((Var x, t):xs)
+
+    replace x t (Var y) | x == y = t
+    replace _ _ t = t
+
 -- | A class for things that contain terms.
 class Symbolic f a | a -> f where
   -- | A different list of all terms contained in the thing.
@@ -169,14 +204,19 @@
     tryApply (typ t) (typ u)
     return (t :$: u)
 
+depth :: Term f -> Int
+depth Var{} = 1
+depth Fun{} = 1
+depth (t :$: u) = depth t `max` (1+depth u)
+
 -- | A standard term ordering - size, skeleton, generality.
 -- Satisfies the property:
 -- if measure (schema t) < measure (schema u) then t < u.
-type Measure f = (Int, Int, Int, MeasureFuns f, Int, [Var])
+type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var])
 -- | Compute the term ordering for a term.
 measure :: (Sized f, Typed f) => Term f -> Measure f
 measure t =
-  (size t, missing t, -length (vars t), MeasureFuns (skel t),
+  (depth t, size t, missing t, -length (vars t), MeasureFuns (skel t),
    -length (usort (vars t)), vars t)
   where
     skel (Var (V ty _)) = Var (V ty 0)
@@ -219,10 +259,6 @@
 instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where
   size (Inl x) = size x
   size (Inr x) = size x
-
-instance (Arity fun1, Arity fun2) => Arity (fun1 :+: fun2) where
-  arity (Inl x) = arity x
-  arity (Inr x) = arity x
 
 instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where
   typ (Inl x) = typ x