diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -17,10 +17,6 @@
   Maybe a new field in args?  Or even things begining with capital letters and
   ":".
 
-* Implement expand by expanding tiers (more robust and flexible).  It
-  will allow extraction of constant values from tiers.  This will also make it
-  easy to amend a Thy: do theorization; add a bunch of atoms; do it again;
-
 
 stranger things (bugs?)
 -----------------------
diff --git a/speculate.cabal b/speculate.cabal
--- a/speculate.cabal
+++ b/speculate.cabal
@@ -1,5 +1,5 @@
 name:                speculate
-version:             0.2.9
+version:             0.2.10
 synopsis:            discovery of properties about Haskell functions
 description:
   Speculate automatically discovers laws about Haskell functions.
@@ -31,7 +31,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/speculate
-  tag:             v0.2.9
+  tag:             v0.2.10
 
 
 library
diff --git a/src/Test/Speculate/Args.hs b/src/Test/Speculate/Args.hs
--- a/src/Test/Speculate/Args.hs
+++ b/src/Test/Speculate/Args.hs
@@ -38,6 +38,7 @@
 import Test.Speculate.Utils
 import System.Console.CmdArgs.Explicit
 
+import Test.LeanCheck ((\/))
 import qualified Data.List as L (insert)
 import Data.List hiding (insert)
 import Data.Maybe (catMaybes)
@@ -59,6 +60,7 @@
   , showSemiequations :: Bool  -- ^ whether to show inequalties
   , showConditions    :: Bool  -- ^ whether to show conditional equations
   , showConstantLaws  :: Bool  -- ^ whether to show laws with no variables
+  , autoConstants     :: Bool  -- ^ automatically include constants taken from tiers of values
 
   , minTests    :: Int -> Int  -- ^ __(intermediary)__ minimum number of tests
                                --   for passing postconditions in function of
@@ -98,6 +100,7 @@
   , maxDepth             = Nothing
   , instances            = []
   , showConstants        = True
+  , autoConstants        = False
   , showArgs             = True
   , showTheory           = False
   , showEquations        = True
@@ -171,15 +174,21 @@
 reallyShowConditions args = showConditions args
                          && boolTy `elem` map (finalResultTy . typ) (allConstants args)
 
-atoms :: Args -> [Expr]
-atoms args = nubSort (map holeOfTy ts)
-     `union` allConstants args
-     `union` [showConstant True  | showConds || showDot args]
-     `union` [showConstant False | showConds || showDot args]
-     `union` (nubSort . catMaybes) [eqE (computeInstances args) t | t <- ts, showConds]
+atoms :: Args -> [[Expr]]
+atoms args = [ nubSort (map holeOfTy ts)
+       `union` allConstants args
+       `union` [showConstant True  | showConds || showDot args]
+       `union` [showConstant False | showConds || showDot args]
+       `union` (nubSort . catMaybes) [eqE is t | showConds, t <- ts] ]
+         \-/ foldr (\/) [] [tiersE is t | autoConstants args, t <- ts]
   where
   ts = types args
+  is = computeInstances args
   showConds = reallyShowConditions args
+  []  \-/ []   =  []
+  xss \-/ []   =  xss
+  []  \-/ yss  =  yss
+  (xs:xss) \-/ (ys:yss)  =  xs `union` ys  :  xss \-/ yss
 
 types :: Args -> [TypeRep]
 types = nubMergeMap (typesIn . typ) . allConstants
@@ -218,7 +227,10 @@
   where
   e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT
   e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT
-  e1 `cmp` e2 = compareIndex (atoms args) e1 e2 <> e1 `compare` e2
+  e1 `cmp` e2 = compareIndex (concat $ atoms args) e1 e2 <> e1 `compare` e2
+-- NOTE: "concat $ atoms args" may be an infinite list.  This function assumes
+-- that the symbols will appear on the list eventually for termination.  If I
+-- am correct this ivariant is assured by the rest of the code.
 
 -- | A special 'Expr' value.
 --   When provided on the 'constants' list, 
@@ -245,6 +257,7 @@
   , "zsemisize"          --= \s a -> a {maxSemiSize = read s}
   , "xcondsize"          --= \s a -> a {maxCondSize = read s}
   , "Aconstants"         --.   \a -> a {showConstants = False} -- TODO: fix name
+  , "Uauto-constants"    --.   \a -> a {autoConstants = True}
   , "Ohide-args"         --.   \a -> a {showArgs = False}
   , "Ttheory"            --.   \a -> a {showTheory = True}
   , "Eno-equations"      --.   \a -> a {showEquations = False}
diff --git a/src/Test/Speculate/Engine.hs b/src/Test/Speculate/Engine.hs
--- a/src/Test/Speculate/Engine.hs
+++ b/src/Test/Speculate/Engine.hs
@@ -14,6 +14,7 @@
   , mostSpecific
 
   , theoryAndRepresentativesFromAtoms
+  , representativesFromAtoms
   , theoryFromAtoms
   , equivalencesBetween
 
@@ -39,6 +40,7 @@
 import Data.Function (on)
 import Data.Monoid ((<>))
 
+import Test.LeanCheck ((\/))
 import Test.Speculate.Utils
 import Test.Speculate.Expr
 import Test.Speculate.Reason
@@ -117,16 +119,19 @@
 -- >     , closureLimit = 2
 -- >     , keepE = keepUpToLength 5
 -- >     }
-theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> Thy
+theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> Thy
 theoryFromAtoms sz cmp keep (===) = fst . theoryAndRepresentativesFromAtoms sz cmp keep (===)
 
-representativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> [Expr]
+representativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]]
 representativesFromAtoms sz cmp keep (===) = snd . theoryAndRepresentativesFromAtoms sz cmp keep (===)
 
-expand :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> (Thy,[Expr]) -> (Thy,[Expr])
-expand keep (===) (thy,ss) = foldl (flip $ consider (===)) (thy,ss)
-                           . concat . zipWithReverse (*$*)
-                           $ collectOn lengthE ss
+expand :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [Expr] -> (Thy,[[Expr]]) -> (Thy,[[Expr]])
+expand keep (===) sz ss (thy,sss) = (complete *** id)
+                                  . foldl (flip $ consider (===) sz) (thy,sss)
+                                  . concat
+                                  . (ss:)
+                                  . zipWithReverse (*$*)
+                                  $ take sz sss
   where
   fes *$* xes = filter keep $ catMaybes [fe $$ xe | fe <- fes, xe <- xes]
 
@@ -135,11 +140,10 @@
 theoryAndRepresentativesFromAtoms :: Int
                                   -> (Expr -> Expr -> Ordering)
                                   -> (Expr -> Bool) -> (Expr -> Expr -> Bool)
-                                  -> [Expr] -> (Thy,[Expr])
-theoryAndRepresentativesFromAtoms sz cmp keep (===) ds =
-  iterate ((complete *** id) . expand keep (===)) dsThy !! (sz-1)
+                                  -> [[Expr]] -> (Thy,[[Expr]])
+theoryAndRepresentativesFromAtoms sz cmp keep (===) dss =
+  chain [expand keep (===) sz' (dss ! (sz'-1)) | sz' <- reverse [1..sz]] (iniThy,[])
   where
-  dsThy = (complete *** id) $ foldl (flip $ consider (===)) (iniThy,[]) ds
   iniThy = emptyThy { keepE = keepUpToLength sz
                     , closureLimit = 2
                     , canReduceTo = dwoBy (\e1 e2 -> e1 `cmp` e2 == GT)
@@ -147,15 +151,21 @@
                     }
 
 -- considers a schema
-consider :: (Expr -> Expr -> Bool) -> Expr -> (Thy,[Expr]) -> (Thy,[Expr])
-consider (===) s (thy,ss)
-  | not (s === s) = (thy,ss++[s])  -- uncomparable type
-  | rehole (normalizeE thy (mostGeneral s)) `elem` ss = (thy,ss)
+consider :: (Expr -> Expr -> Bool) -> Int -> Expr -> (Thy,[[Expr]]) -> (Thy,[[Expr]])
+consider (===) sz s (thy,sss)
+  | not (s === s) = (thy,sssWs)  -- uncomparable type
+  | rehole (normalizeE thy (mostGeneral s)) `elem` ss = (thy,sss)
   | otherwise =
     ( append thy $ equivalencesBetween (===) s s ++ eqs
-    , ss ++ [s | not $ any (\(e1,e2) -> unrepeatedVars e1 && unrepeatedVars e2) eqs])
+    , if any (\(e1,e2) -> unrepeatedVars e1 && unrepeatedVars e2) eqs
+        then sss
+        else sssWs )
     where
+    ss = uptoT sz sss
+    sssWs = sss \/ wcons0 sz s
     eqs = concatMap (equivalencesBetween (===) s) $ filter (s ===) ss
+    wcons0 :: Int -> a -> [[a]]
+    wcons0 n s = replicate (n-1) [] ++ [[s]]
 
 distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr]
 distinctFromSchemas ti nt nv thy = map C.rep . classesFromSchemas ti nt nv thy
diff --git a/src/Test/Speculate/Report.hs b/src/Test/Speculate/Report.hs
--- a/src/Test/Speculate/Report.hs
+++ b/src/Test/Speculate/Report.hs
@@ -33,10 +33,12 @@
   let ti = computeInstances args
   let ats = types args
   let ts = filter (isListable ti) ats
-  let ds' = atoms args
-  let (thy,es) = theoryAndRepresentativesFromAtoms sz (compareExpr args) (keepExpr args) (timeout args .: equal ti n) ds'
+  let dss = atoms args
+  let (thy,ess) = theoryAndRepresentativesFromAtoms sz (compareExpr args) (keepExpr args) (timeout args .: equal ti n) dss
+  let es = uptoT sz ess
   putArgs args
-  when (showConstants args)    . putStrLn . unlines $ map show ds'
+  -- TODO: somehow show the tail of dss, maybe use "..."
+  when (showConstants args) . putStrLn . unlines $ map show (head dss)
   warnMissingInstances ti ats
   let ies = instanceErrors ti n ats
   unless (null ies) $ do
diff --git a/src/Test/Speculate/Sanity.hs b/src/Test/Speculate/Sanity.hs
--- a/src/Test/Speculate/Sanity.hs
+++ b/src/Test/Speculate/Sanity.hs
@@ -64,7 +64,7 @@
   ++ [ "(<=) :: " ++ ty ++ "  is not an ordering ("     ++ intercalate ", " es ++ ")"
      | let es = ordErrors is n t, isOrd is t, not (null es) ]
   ++ [ "(==) and (<=) :: " ++ ty ++ " are inconsistent: (x == y) /= (x <= y && y <= x)"
-     | f $ (x -==- y) -==- (x -<=- y -&&- y -<=- x)]
+     | f $ (x -==- y) -==- (x -<=- y -&&- y -<=- x), isEq is t, isOrd is t ]
   where
   f = not . true is n
   x = Var "x" t
diff --git a/src/Test/Speculate/Utils/List.hs b/src/Test/Speculate/Utils/List.hs
--- a/src/Test/Speculate/Utils/List.hs
+++ b/src/Test/Speculate/Utils/List.hs
@@ -30,6 +30,7 @@
   , takeGreaterHalf
   , accum
   , partitionByMarkers
+  , (!)
   )
 where
 
@@ -215,3 +216,10 @@
       | x == y -> let (ys',zs') = partitionByMarkers y z zs in (ys++ys',zs')
       | x == z -> let (zs',ys') = partitionByMarkers z y zs in (ys++ys',zs')
       | otherwise -> error "partitionByMarkers: the impossible happened, this is definitely a bug.  See source."
+
+-- Total version of !! that works on lists of lists (returning [] for index not
+-- found).
+(!) :: [[a]] -> Int -> [a]
+(xs:xss) ! 0  =  xs
+(xs:xss) ! n  =  xss ! (n-1)
+[]       ! n  =  []
diff --git a/tests/test-utils.hs b/tests/test-utils.hs
--- a/tests/test-utils.hs
+++ b/tests/test-utils.hs
@@ -126,4 +126,7 @@
   , holds n $ \xs ys -> xs +++ ys == ys +++ (xs :: [Int])
   , holds n $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys
                     ==> xs +++ ys == nubSort (xs ++ ys :: [Int])
+
+  , holds n $ \n xss -> 0 <  n && n <  length xss ==> xss ! n == (xss !! n :: [Int])
+  , holds n $ \n xss -> 0 >= n && n >= length xss ==> xss ! n == ([] :: [Int])
   ]