diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -29,11 +29,15 @@
 # benches, prototypes and test programs
 eg/arith
 eg/bools
+eg/count
 eg/factorial
 eg/fibonacci
 eg/ints
+eg/gcd
 eg/list
 eg/tapps
+eg/tree
+eg/setelem
 eg/spec
 bench/self
 bench/longshot
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -7,13 +7,17 @@
 
 EG = \
   eg/arith \
+  eg/count \
   eg/factorial \
   eg/fibonacci \
   eg/ints \
   eg/bools \
+  eg/gcd \
   eg/list \
+  eg/setelem \
   eg/spec \
   eg/tapps \
+  eg/tree \
   bench/ill-hit \
   bench/longshot \
   bench/self \
@@ -47,7 +51,7 @@
 
 diff-test: $(patsubst %,%.diff-test,$(EG))
 
-update-diff-test: $(patsubst %,%.update-diff-test,$(EG))
+out: $(patsubst %,%.out,$(EG))
 
 test-sdist:
 	./test/sdist
@@ -64,7 +68,7 @@
 	echo 'Unsupported'
 
 clean: clean-hi-o clean-haddock
-	rm -f $(EG) $(TESTS)
+	rm -f $(EG) $(TESTS) mk/toplibs
 
 full-clean: clean clean-cabal clean-stack
 	rm -f tags TAGS mk/toplibs
@@ -72,11 +76,11 @@
 %.run: %
 	./$<
 
-%.diff-test: %
-	./$< | diff -rud test/model/$<.out -
+%.out: %
+	./$< >$<.out
 
-%.update-diff-test: %
-	./$< >           test/model/$<.out
+%.diff-test: %
+	./$< | diff -rud $<.out -
 
 # lists files missing copyright notices
 list-missing-copyright:
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,23 +3,21 @@
 
 A non-exhaustive list of things TO DO for Conjure.
 
+* think about how can we allow gcd to be produced
 
-* top-down generation of candidate expressions
+* use holes for recursions, code will probably become cleaner
+  (and possibly faster)
 
 * generate functions with top-level case patterns:
 
         len []  =  0
         len (x:xs)  =  1 + len xs
 
-* only allow recursion on deconstructed arguments:
 
-        foo (x:xs)  =  ... len xs ...
-
-  this will require generation of functions with top-level case patterns.
-
-
 ### for later
 
+* allow recursion under any lazy functions (discover them by testing!)
+
 * exclude magic numbers?  e.g.: `1+1`?
 
 * allow conjuring from partially defined implementations?
@@ -31,9 +29,14 @@
                   then 1
                   else impl f n
 
+* consider discover orderings on arguments?
+
 * consider leveraging lazyness somehow?
+  (related to allowing recursion under any lazy functions)
 
 * consider leveraging polymorphism somehow?
+
+* consider allowing lambdas that introduce free variables?
 
 
 This file is part of Conjure,
diff --git a/bench/ill-hit.out b/bench/ill-hit.out
new file mode 100644
--- /dev/null
+++ b/bench/ill-hit.out
@@ -0,0 +1,42 @@
+sum :: [Int] -> Int
+-- testing 4 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 5 candidates of size 6
+-- looking through 15 candidates of size 7
+-- looking through 27 candidates of size 8
+-- looking through 53 candidates of size 9
+-- looking through 101 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+sum :: [Int] -> Int
+-- testing 6 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 5 candidates of size 6
+-- looking through 15 candidates of size 7
+-- looking through 27 candidates of size 8
+-- looking through 53 candidates of size 9
+-- looking through 101 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+sum :: [Int] -> Int
+-- testing 6 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 5 candidates of size 6
+-- looking through 15 candidates of size 7
+-- looking through 27 candidates of size 8
+-- looking through 53 candidates of size 9
+-- looking through 101 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
diff --git a/bench/longshot.hs b/bench/longshot.hs
--- a/bench/longshot.hs
+++ b/bench/longshot.hs
@@ -21,6 +21,25 @@
 pow 2 3  =  8
 pow 3 2  =  9
 
+duplicates :: [Int] -> [Int] -- Eq a => [a] -> [a]
+duplicates []  =  []
+duplicates (x:xs)  =
+  if x `elem` xs && not (x `elem` d)
+  then x : d
+  else d
+  where
+  d  =  duplicates xs
+
+positionsFrom :: Int -> Int -> [Int] -> [Int]
+positionsFrom n x  =  from n
+  where
+  from _ []  =  []
+  from n (y:ys)  =  if y == x
+                    then n : f
+                    else f
+    where
+    f  =  from (n+1) ys
+
 main :: IO ()
 main = do
   -- qsort
@@ -65,5 +84,39 @@
     , value "+" ((+) :: Int -> Int -> Int)
     , value "*" ((*) :: Int -> Int -> Int)
     , value "halve" ((`div` 2) :: Int -> Int)
+    , value "==" ((==) :: Int -> Int -> Bool)
+    ]
+
+  -- duplicates xs  =
+  --   if null xs                                                                   --  3
+  --   then []                                                                      --  4
+  --   else if head xs `elem` tail xs && not (head xs `elem` duplicates (tail xs))  -- 18
+  --        then head xs : duplicates (tail xs)                                     -- 24
+  --        else duplicates (tail xs)                                               -- 27
+  conjure "duplicates" duplicates
+    [ val ([] :: [Int])
+    , val True
+    , val False
+    , value "not" not
+    , value "||" (||)
+    , value "&&" (&&)
+    , value ":" ((:) :: Int -> [Int] -> [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "null" (null :: [Int] -> Bool)
+    , value "elem" (elem :: Int -> [Int] -> Bool)
+    ]
+
+  conjure "positionsFrom" positionsFrom
+    [ val ([] :: [Int])
+    , val True
+    , val False
+    , value "not" not
+    , value "||" (||)
+    , value "&&" (&&)
+    , value ":" ((:) :: Int -> [Int] -> [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "null" (null :: [Int] -> Bool)
     , value "==" ((==) :: Int -> Int -> Bool)
     ]
diff --git a/bench/longshot.out b/bench/longshot.out
new file mode 100644
--- /dev/null
+++ b/bench/longshot.out
@@ -0,0 +1,72 @@
+qsort :: [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 11 candidates of size 4
+-- looking through 28 candidates of size 5
+-- looking through 72 candidates of size 6
+-- looking through 207 candidates of size 7
+-- looking through 611 candidates of size 8
+-- looking through 1779 candidates of size 9
+-- looking through 5301 candidates of size 10
+-- looking through 16103 candidates of size 11
+-- looking through 49113 candidates of size 12
+cannot conjure
+
+pow :: Int -> Int -> Int
+-- testing 5 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 13 candidates of size 3
+-- looking through 20 candidates of size 4
+-- looking through 80 candidates of size 5
+-- looking through 172 candidates of size 6
+-- looking through 614 candidates of size 7
+-- looking through 1623 candidates of size 8
+cannot conjure
+
+pow :: Int -> Int -> Int
+-- testing 5 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 15 candidates of size 3
+-- looking through 26 candidates of size 4
+-- looking through 111 candidates of size 5
+-- looking through 307 candidates of size 6
+-- looking through 1122 candidates of size 7
+-- looking through 3675 candidates of size 8
+cannot conjure
+
+duplicates :: [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 10 candidates of size 5
+-- looking through 14 candidates of size 6
+-- looking through 30 candidates of size 7
+-- looking through 70 candidates of size 8
+-- looking through 154 candidates of size 9
+-- looking through 366 candidates of size 10
+-- looking through 914 candidates of size 11
+-- looking through 2234 candidates of size 12
+cannot conjure
+
+positionsFrom :: Int -> Int -> [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 6 candidates of size 3
+-- looking through 10 candidates of size 4
+-- looking through 22 candidates of size 5
+-- looking through 42 candidates of size 6
+-- looking through 86 candidates of size 7
+-- looking through 170 candidates of size 8
+-- looking through 358 candidates of size 9
+-- looking through 810 candidates of size 10
+-- looking through 2046 candidates of size 11
+-- looking through 5578 candidates of size 12
+cannot conjure
+
diff --git a/bench/runtime/zero/bench/ill-hit.runtime b/bench/runtime/zero/bench/ill-hit.runtime
--- a/bench/runtime/zero/bench/ill-hit.runtime
+++ b/bench/runtime/zero/bench/ill-hit.runtime
@@ -1,1 +1,1 @@
-1.2
+1.1
diff --git a/bench/runtime/zero/bench/longshot.runtime b/bench/runtime/zero/bench/longshot.runtime
--- a/bench/runtime/zero/bench/longshot.runtime
+++ b/bench/runtime/zero/bench/longshot.runtime
@@ -1,1 +1,1 @@
-2.7
+4.3
diff --git a/bench/runtime/zero/bench/take-drop.runtime b/bench/runtime/zero/bench/take-drop.runtime
--- a/bench/runtime/zero/bench/take-drop.runtime
+++ b/bench/runtime/zero/bench/take-drop.runtime
@@ -1,1 +1,1 @@
-5.7
+5.8
diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime
--- a/bench/runtime/zero/eg/arith.runtime
+++ b/bench/runtime/zero/eg/arith.runtime
@@ -1,1 +1,1 @@
-0.9
+0.8
diff --git a/bench/runtime/zero/eg/bools.runtime b/bench/runtime/zero/eg/bools.runtime
--- a/bench/runtime/zero/eg/bools.runtime
+++ b/bench/runtime/zero/eg/bools.runtime
@@ -1,1 +1,1 @@
-3.1
+2.8
diff --git a/bench/runtime/zero/eg/count.runtime b/bench/runtime/zero/eg/count.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/count.runtime
@@ -0,0 +1,1 @@
+2.3
diff --git a/bench/runtime/zero/eg/fibonacci.runtime b/bench/runtime/zero/eg/fibonacci.runtime
--- a/bench/runtime/zero/eg/fibonacci.runtime
+++ b/bench/runtime/zero/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-2.7
+20.8
diff --git a/bench/runtime/zero/eg/gcd.runtime b/bench/runtime/zero/eg/gcd.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/gcd.runtime
@@ -0,0 +1,1 @@
+0.3
diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime
--- a/bench/runtime/zero/eg/list.runtime
+++ b/bench/runtime/zero/eg/list.runtime
@@ -1,1 +1,1 @@
-0.6
+0.4
diff --git a/bench/runtime/zero/eg/setelem.runtime b/bench/runtime/zero/eg/setelem.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/setelem.runtime
@@ -0,0 +1,1 @@
+23.3
diff --git a/bench/runtime/zero/eg/spec.runtime b/bench/runtime/zero/eg/spec.runtime
--- a/bench/runtime/zero/eg/spec.runtime
+++ b/bench/runtime/zero/eg/spec.runtime
@@ -1,1 +1,1 @@
-0.5
+0.4
diff --git a/bench/runtime/zero/eg/tree.runtime b/bench/runtime/zero/eg/tree.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/tree.runtime
@@ -0,0 +1,1 @@
+4.6
diff --git a/bench/runtime/zero/proto/u-conjure.runtime b/bench/runtime/zero/proto/u-conjure.runtime
--- a/bench/runtime/zero/proto/u-conjure.runtime
+++ b/bench/runtime/zero/proto/u-conjure.runtime
@@ -1,1 +1,1 @@
-0.4
+0.3
diff --git a/bench/runtime/zero/versions b/bench/runtime/zero/versions
--- a/bench/runtime/zero/versions
+++ b/bench/runtime/zero/versions
@@ -1,4 +1,4 @@
 GHC 8.10.4
-leancheck-0.9.6
-express-0.1.12
-speculate-0.4.6
+leancheck-0.9.10
+express-0.1.14
+speculate-0.4.8
diff --git a/bench/self.out b/bench/self.out
new file mode 100644
--- /dev/null
+++ b/bench/self.out
@@ -0,0 +1,28 @@
+(?) :: Int -> Int -> Int
+-- testing 60 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 32 candidates of size 3
+x ? y  =  x + y
+
+(?) :: Int -> Int -> Int
+-- testing 60 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 32 candidates of size 3
+x ? y  =  x * y
+
+i :: Int -> Int
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 18 candidates of size 3
+i x  =  x + 1
+
+d :: Int -> Int
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 18 candidates of size 3
+cannot conjure
+
diff --git a/bench/take-drop.out b/bench/take-drop.out
new file mode 100644
--- /dev/null
+++ b/bench/take-drop.out
@@ -0,0 +1,37 @@
+drop :: Int -> [A] -> [A]
+-- testing 60 combinations of argument values
+-- looking through 1 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 1 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 1 candidates of size 6
+-- looking through 1 candidates of size 7
+-- looking through 7 candidates of size 8
+-- looking through 33 candidates of size 9
+-- looking through 100 candidates of size 10
+-- looking through 236 candidates of size 11
+-- looking through 510 candidates of size 12
+-- looking through 1069 candidates of size 13
+drop x xs  =  if null xs || x == 0 then xs else drop (dec x) (tail xs)
+
+take :: Int -> [A] -> [A]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 10 candidates of size 5
+-- looking through 14 candidates of size 6
+-- looking through 26 candidates of size 7
+-- looking through 62 candidates of size 8
+-- looking through 176 candidates of size 9
+-- looking through 470 candidates of size 10
+-- looking through 1190 candidates of size 11
+-- looking through 3116 candidates of size 12
+-- looking through 8020 candidates of size 13
+-- looking through 19658 candidates of size 14
+-- looking through 46906 candidates of size 15
+-- looking through 109976 candidates of size 16
+take x xs  =  if null xs || x == 0 then [] else head xs:take (dec x) (tail xs)
+
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,18 @@
 ============================
 
 
+v0.3.4
+------
+
+* reallow recursions under `&&` and `||`
+  (simplifies the generated `or`, `and`, `set` and `elem` functions)
+* only require deconstructions on a non-empty subset of arguments
+  (allows `fib01` to be produced)
+* limit number of terminal evaluations in `recursiveToDynamic`
+* fix bug in `recursiveToDynamic` (not counting some recursions)
+* add 4 new benchmarks: `count`, `gcd`, `tree` and `setelem`
+
+
 v0.3.2
 ------
 
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -3,7 +3,7 @@
 -- Copyright (C) 2021 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.3.2
+version:             0.3.4
 synopsis:            conjure Haskell functions out of partial definitions
 description:
   Conjure is a tool that produces Haskell functions out of partial definitions.
@@ -29,8 +29,11 @@
                   , .github/workflows/build.yml
                   , Makefile
                   , bench/*.hs
+                  , bench/*.out
                   , eg/*.hs
+                  , eg/*.out
                   , proto/*.hs
+                  , proto/*.out
                   , mk/All.hs
                   , mk/Toplibs.hs
                   , mk/depend.mk
@@ -44,9 +47,6 @@
                   , bench/runtime/zero/proto/*.runtime
                   , bench/runtime/zero/versions
                   , bench/versions
-                  , test/model/bench/*.out
-                  , test/model/eg/*.out
-                  , test/model/proto/*.out
                   , test/sdist
 tested-with: GHC==9.0
            , GHC==8.10
@@ -65,7 +65,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.3.2
+  tag:             v0.3.4
 
 library
   exposed-modules: Conjure
@@ -74,13 +74,13 @@
                  , Conjure.Expr
                  , Conjure.Spec
                  , Conjure.Utils
-                 , Conjure.Constructors
+                 , Conjure.Cases
   other-extensions: TemplateHaskell, CPP
   build-depends: base >= 4 && < 5
-               , leancheck >= 0.9.6
+               , leancheck >= 0.9.10
                , template-haskell
-               , speculate >= 0.4.6
-               , express >= 0.1.12
+               , speculate >= 0.4.8
+               , express >= 0.1.14
   hs-source-dirs:      src
   default-language:    Haskell2010
 
diff --git a/eg/arith.out b/eg/arith.out
new file mode 100644
--- /dev/null
+++ b/eg/arith.out
@@ -0,0 +1,32 @@
+double :: Int -> Int
+-- testing 4 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 5 candidates of size 3
+double x  =  x + x
+
+add :: Int -> Int -> Int
+-- testing 4 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 13 candidates of size 3
+add x y  =  x + y
+
+square :: Int -> Int
+-- testing 3 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 5 candidates of size 3
+square x  =  x * x
+
+tnpo :: Int -> Int
+-- testing 3 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 5 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 13 candidates of size 5
+-- looking through 0 candidates of size 6
+-- looking through 42 candidates of size 7
+tnpo x  =  x + (x + (x + 1))
+
diff --git a/eg/bools.out b/eg/bools.out
new file mode 100644
--- /dev/null
+++ b/eg/bools.out
@@ -0,0 +1,43 @@
+and :: [Bool] -> Bool
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 4 candidates of size 4
+-- looking through 6 candidates of size 5
+-- looking through 19 candidates of size 6
+-- looking through 45 candidates of size 7
+-- looking through 80 candidates of size 8
+-- looking through 156 candidates of size 9
+and ps  =  null ps || head ps && and (tail ps)
+
+or :: [Bool] -> Bool
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 4 candidates of size 4
+-- looking through 6 candidates of size 5
+-- looking through 19 candidates of size 6
+-- looking through 45 candidates of size 7
+-- looking through 80 candidates of size 8
+-- looking through 156 candidates of size 9
+-- looking through 382 candidates of size 10
+or ps  =  not (null ps) && (head ps || or (tail ps))
+
+and :: [Bool] -> Bool
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 6 candidates of size 4
+and ps  =  foldr (&&) True ps
+
+or :: [Bool] -> Bool
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 6 candidates of size 4
+or ps  =  foldr (||) False ps
+
diff --git a/eg/count.hs b/eg/count.hs
new file mode 100644
--- /dev/null
+++ b/eg/count.hs
@@ -0,0 +1,43 @@
+-- count.hs: elem and set functions
+import Conjure
+
+count :: Eq a => a -> [a] -> Int
+count x  =  c
+  where
+  c []  =  0
+  c (y:ys)  =  (if x == y then 1 else 0) + c ys
+
+-- this is the expected function
+countIf :: A -> [A] -> Int
+countIf x xs  =  if null xs                                                 -- 3
+                 then 0                                                     -- 4
+                 else (if x == head xs then 1 else 0) + countIf x (tail xs) -- 16
+                 --    5  6 7   8   9      10     11 12   13   14   15  16
+
+count' :: A -> [A] -> Int
+count' 0 [0]  =  1
+count' 0 [1]  =  0
+count' 1 [0]  =  0
+count' 1 [1]  =  1
+count' 0 [0,0]  =  2
+count' 0 [0,1]  =  1
+count' 0 [1,2]  =  0
+count' 1 [0,0]  =  0
+count' 1 [0,1]  =  1
+count' 1 [1,2]  =  1
+count' 0 [0,0,0]  =  3
+count' 0 [0,0,1]  =  2
+count' 0 [1,0,0]  =  2
+
+main :: IO ()
+main = do
+  conjureWithMaxSize 16 "count" count'
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "head" (head :: [A] -> A)
+    , value "tail" (tail :: [A] -> [A])
+    , value "null" (null :: [A] -> Bool)
+    , value "==" ((==) :: A -> A -> Bool)
+    , value "if" (\p x y -> if p then x else y :: Int)
+    ]
diff --git a/eg/count.out b/eg/count.out
new file mode 100644
--- /dev/null
+++ b/eg/count.out
@@ -0,0 +1,20 @@
+count :: A -> [A] -> Int
+-- testing 13 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 3 candidates of size 5
+-- looking through 2 candidates of size 6
+-- looking through 13 candidates of size 7
+-- looking through 16 candidates of size 8
+-- looking through 57 candidates of size 9
+-- looking through 84 candidates of size 10
+-- looking through 242 candidates of size 11
+-- looking through 401 candidates of size 12
+-- looking through 1045 candidates of size 13
+-- looking through 1895 candidates of size 14
+-- looking through 4672 candidates of size 15
+-- looking through 8990 candidates of size 16
+count x xs  =  if null xs then 0 else count x (tail xs) + (if x == head xs then 1 else 0)
+
diff --git a/eg/factorial.out b/eg/factorial.out
new file mode 100644
--- /dev/null
+++ b/eg/factorial.out
@@ -0,0 +1,22 @@
+factorial :: Int -> Int
+-- testing 6 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 0 candidates of size 3
+-- looking through 2 candidates of size 4
+factorial n  =  product (enumFromTo 1 n)
+
+factorial :: Int -> Int
+-- testing 6 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 5 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 20 candidates of size 5
+-- looking through 27 candidates of size 6
+-- looking through 87 candidates of size 7
+-- looking through 167 candidates of size 8
+-- looking through 417 candidates of size 9
+-- looking through 960 candidates of size 10
+factorial n  =  if n == 0 then 1 else n * factorial (dec n)
+
diff --git a/eg/fibonacci.hs b/eg/fibonacci.hs
--- a/eg/fibonacci.hs
+++ b/eg/fibonacci.hs
@@ -11,6 +11,16 @@
 fibonacci 6  =  13
 fibonacci 7  =  21
 
+fib01 :: Int -> Int -> Int -> Int
+fib01 0 1 0  =  1
+fib01 0 1 1  =  1
+fib01 0 1 2  =  2
+fib01 0 1 3  =  3
+fib01 0 1 4  =  5
+fib01 0 1 5  =  8
+fib01 0 1 6  =  13
+fib01 0 1 7  =  21
+
 as :: Args
 as  =  args{maxSize=13,maxRecursiveCalls=2}
 
@@ -25,3 +35,13 @@
 -- expected function:
 -- fibonacci n  =  if n <= 1 then 1 else fibonacci (dec n) + fibonacci (dec (dec n))
 --                 1  2 3  4      5      6          7   8  9        10  11   12  13
+
+  conjureWithMaxSize 12 "fib01" fib01
+    [ val (0::Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "dec" (subtract 1 :: Int -> Int)
+    , value "<=" ((<=) :: Int -> Int -> Bool)
+    ]
+-- expected function:
+-- fib01 x y z  =  if z <= 0 then y else fib01 y (x + y) (dec z)
+--                 1  2 3  4      5      6     7  8 9 10  11 12
diff --git a/eg/fibonacci.out b/eg/fibonacci.out
new file mode 100644
--- /dev/null
+++ b/eg/fibonacci.out
@@ -0,0 +1,33 @@
+fibonacci :: Int -> Int
+-- testing 8 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 6 candidates of size 3
+-- looking through 1 candidates of size 4
+-- looking through 11 candidates of size 5
+-- looking through 5 candidates of size 6
+-- looking through 27 candidates of size 7
+-- looking through 20 candidates of size 8
+-- looking through 95 candidates of size 9
+-- looking through 140 candidates of size 10
+-- looking through 407 candidates of size 11
+-- looking through 825 candidates of size 12
+-- looking through 2153 candidates of size 13
+fibonacci n  =  if n <= 1 then 1 else fibonacci (dec n) + fibonacci (dec (dec n))
+
+fib01 :: Int -> Int -> Int -> Int
+-- testing 8 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 4 candidates of size 2
+-- looking through 9 candidates of size 3
+-- looking through 21 candidates of size 4
+-- looking through 43 candidates of size 5
+-- looking through 84 candidates of size 6
+-- looking through 192 candidates of size 7
+-- looking through 391 candidates of size 8
+-- looking through 840 candidates of size 9
+-- looking through 9294 candidates of size 10
+-- looking through 37807 candidates of size 11
+-- looking through 166308 candidates of size 12
+fib01 x y z  =  if z <= 0 then y else fib01 y (x + y) (dec z)
+
diff --git a/eg/gcd.hs b/eg/gcd.hs
new file mode 100644
--- /dev/null
+++ b/eg/gcd.hs
@@ -0,0 +1,29 @@
+-- gcd.hs: conjuring a GCD implementation
+--
+-- Copyright (C) 2021 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+import Conjure
+
+gcd' :: Int -> Int -> Int
+gcd' 1 1  =  1
+gcd' 1 2  =  1
+gcd' 2 1  =  1
+gcd' 2 2  =  2
+gcd' 2 6  =  2
+gcd' 6 2  =  2
+gcd' 3 6  =  3
+gcd' 6 3  =  3
+gcd' 6 9  =  3
+gcd' 9 6  =  3
+gcd' 12 18  =  6
+
+main :: IO ()
+main = conjure "gcd a b" gcd'
+  [ val (0::Int)
+  , value "`mod`" (mod :: Int -> Int -> Int)
+  , value "==" ((==) :: Int -> Int -> Bool)
+  ]
+  -- desired function:
+  -- gcd a b  =  if b == 0 then a else gcd b (a `mod` b)
+  --             1  2 3  4      5      6   7  8  9   10
+  -- TODO: make it so that conjure is able to find this
diff --git a/eg/gcd.out b/eg/gcd.out
new file mode 100644
--- /dev/null
+++ b/eg/gcd.out
@@ -0,0 +1,16 @@
+gcd :: Int -> Int -> Int
+-- testing 11 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 9 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 54 candidates of size 5
+-- looking through 0 candidates of size 6
+-- looking through 405 candidates of size 7
+-- looking through 0 candidates of size 8
+-- looking through 3402 candidates of size 9
+-- looking through 0 candidates of size 10
+-- looking through 30618 candidates of size 11
+-- looking through 0 candidates of size 12
+cannot conjure
+
diff --git a/eg/ints.out b/eg/ints.out
new file mode 100644
--- /dev/null
+++ b/eg/ints.out
@@ -0,0 +1,59 @@
+second :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+second xs  =  head (tail xs)
+
+third :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+third xs  =  head (tail (tail xs))
+
+sum :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 5 candidates of size 6
+-- looking through 15 candidates of size 7
+-- looking through 27 candidates of size 8
+-- looking through 53 candidates of size 9
+-- looking through 101 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+product :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 5 candidates of size 6
+-- looking through 15 candidates of size 7
+-- looking through 27 candidates of size 8
+-- looking through 53 candidates of size 9
+-- looking through 101 candidates of size 10
+product xs  =  if null xs then 1 else head xs * product (tail xs)
+
+sum :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 5 candidates of size 4
+sum xs  =  foldr (+) 0 xs
+
+product :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 5 candidates of size 4
+product xs  =  foldr (*) 1 xs
+
diff --git a/eg/list.out b/eg/list.out
new file mode 100644
--- /dev/null
+++ b/eg/list.out
@@ -0,0 +1,109 @@
+length :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 0 candidates of size 6
+-- looking through 5 candidates of size 7
+-- looking through 8 candidates of size 8
+-- looking through 19 candidates of size 9
+length xs  =  if null xs then 0 else 1 + length (tail xs)
+
+reverse :: [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 5 candidates of size 3
+-- looking through 9 candidates of size 4
+-- looking through 23 candidates of size 5
+-- looking through 57 candidates of size 6
+-- looking through 147 candidates of size 7
+-- looking through 381 candidates of size 8
+-- looking through 1014 candidates of size 9
+-- looking through 2736 candidates of size 10
+-- looking through 7447 candidates of size 11
+reverse xs  =  if null xs then xs else reverse (tail xs) ++ unit (head xs)
+
+sort :: [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 11 candidates of size 5
+-- looking through 21 candidates of size 6
+-- looking through 49 candidates of size 7
+-- looking through 119 candidates of size 8
+-- looking through 272 candidates of size 9
+-- looking through 625 candidates of size 10
+sort xs  =  if null xs then xs else insert (head xs) (sort (tail xs))
+
+(++) :: [Int] -> [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 12 candidates of size 4
+-- looking through 21 candidates of size 5
+-- looking through 30 candidates of size 6
+-- looking through 66 candidates of size 7
+-- looking through 225 candidates of size 8
+-- looking through 723 candidates of size 9
+-- looking through 1965 candidates of size 10
+-- looking through 5544 candidates of size 11
+xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
+
+length :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 7 candidates of size 6
+length xs  =  foldr (const (1 +)) 0 xs
+
+reverse :: [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 8 candidates of size 6
+-- looking through 13 candidates of size 7
+reverse xs  =  foldr (flip (++) . unit) [] xs
+
+sort :: [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 0 candidates of size 3
+-- looking through 2 candidates of size 4
+sort xs  =  foldr insert [] xs
+
+(++) :: [Int] -> [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 0 candidates of size 3
+-- looking through 4 candidates of size 4
+xs ++ ys  =  foldr (:) ys xs
+
+(\/) :: [Int] -> [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 12 candidates of size 4
+-- looking through 21 candidates of size 5
+-- looking through 30 candidates of size 6
+-- looking through 66 candidates of size 7
+-- looking through 225 candidates of size 8
+-- looking through 723 candidates of size 9
+-- looking through 1965 candidates of size 10
+-- looking through 5544 candidates of size 11
+xs \/ ys  =  if null xs then xs else head xs:ys \/ tail xs
+
diff --git a/eg/setelem.hs b/eg/setelem.hs
new file mode 100644
--- /dev/null
+++ b/eg/setelem.hs
@@ -0,0 +1,44 @@
+-- setelem.hs: elem and set functions
+import Conjure
+
+elem' :: Int -> [Int] -> Bool
+elem' x [y]  =  x == y
+elem' x [y,z]  =  x == y || x == z
+elem' x [y,z,w]  =  x == y || x == z || x == w
+
+set' :: [Int] -> Bool
+set' [x]  =  True
+set' [x,y]  =  not (x == y)
+set' [x,y,z]  =  not (x == y || y == z || x == z)
+
+main :: IO ()
+main = do
+  -- elem x xs  =  if null xs then False else elem x (tail xs) || x == head xs
+  conjureWithMaxSize 13 "elem" (elem')
+    [ val ([] :: [Int])
+    , val True
+    , val False
+    , value "not" not
+    , value "||" (||)
+    , value "&&" (&&)
+    , value ":" ((:) :: Int -> [Int] -> [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "null" (null :: [Int] -> Bool)
+    , value "==" ((==) :: Int -> Int -> Bool)
+    ]
+
+  -- set xs  =  if null xs then True else not (head xs `elem` tail xs) && set (tail xs)
+  conjureWithMaxSize 14 "set" (set')
+    [ val ([] :: [Int])
+    , val True
+    , val False
+    , value "not" not
+    , value "||" (||)
+    , value "&&" (&&)
+    , value ":" ((:) :: Int -> [Int] -> [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "null" (null :: [Int] -> Bool)
+    , value "elem" (elem :: Int -> [Int] -> Bool)
+    ]
diff --git a/eg/setelem.out b/eg/setelem.out
new file mode 100644
--- /dev/null
+++ b/eg/setelem.out
@@ -0,0 +1,35 @@
+elem :: Int -> [Int] -> Bool
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 8 candidates of size 4
+-- looking through 14 candidates of size 5
+-- looking through 25 candidates of size 6
+-- looking through 57 candidates of size 7
+-- looking through 137 candidates of size 8
+-- looking through 320 candidates of size 9
+-- looking through 720 candidates of size 10
+-- looking through 1737 candidates of size 11
+-- looking through 4204 candidates of size 12
+-- looking through 10333 candidates of size 13
+elem x xs  =  not (null xs) && (elem x (tail xs) || x == head xs)
+
+set :: [Int] -> Bool
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 5 candidates of size 4
+-- looking through 11 candidates of size 5
+-- looking through 26 candidates of size 6
+-- looking through 61 candidates of size 7
+-- looking through 142 candidates of size 8
+-- looking through 302 candidates of size 9
+-- looking through 692 candidates of size 10
+-- looking through 1651 candidates of size 11
+-- looking through 3945 candidates of size 12
+-- looking through 9309 candidates of size 13
+-- looking through 22246 candidates of size 14
+set xs  =  not (elem (head xs) (tail xs)) && (null (tail xs) || set (tail xs))
+
diff --git a/eg/spec.out b/eg/spec.out
new file mode 100644
--- /dev/null
+++ b/eg/spec.out
@@ -0,0 +1,29 @@
+sum :: [Int] -> Int
+-- testing 3 combinations of argument values
+-- looking through 1 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 1 candidates of size 4
+-- looking through 2 candidates of size 5
+-- looking through 2 candidates of size 6
+-- looking through 5 candidates of size 7
+-- looking through 10 candidates of size 8
+-- looking through 17 candidates of size 9
+-- looking through 28 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+(++) :: [Int] -> [Int] -> [Int]
+-- testing 3 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 10 candidates of size 5
+-- looking through 14 candidates of size 6
+-- looking through 26 candidates of size 7
+-- looking through 94 candidates of size 8
+-- looking through 298 candidates of size 9
+-- looking through 766 candidates of size 10
+-- looking through 2010 candidates of size 11
+xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
+
diff --git a/eg/tapps.out b/eg/tapps.out
new file mode 100644
--- /dev/null
+++ b/eg/tapps.out
@@ -0,0 +1,30 @@
+third :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+third xs  =  head (tail (tail xs))
+
+product :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 5 candidates of size 6
+-- looking through 15 candidates of size 7
+-- looking through 27 candidates of size 8
+-- looking through 53 candidates of size 9
+-- looking through 101 candidates of size 10
+product xs  =  if null xs then 1 else head xs * product (tail xs)
+
+product :: [Int] -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 5 candidates of size 4
+product xs  =  foldr (*) 1 xs
+
diff --git a/eg/tree.hs b/eg/tree.hs
new file mode 100644
--- /dev/null
+++ b/eg/tree.hs
@@ -0,0 +1,165 @@
+-- tree.hs: conjuring functions over trees
+--
+-- Copyright (C) 2021 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ == 708
+{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving #-}
+import Data.Typeable (Typeable)
+#endif
+
+import Conjure
+import Test.LeanCheck
+
+data Tree  =  Leaf
+           |  Node Tree Int Tree
+  deriving (Eq, Ord, Show, Read)
+
+#if __GLASGOW_HASKELL__ == 708
+deriving instance Typeable Tree
+#endif
+
+unit :: Int -> Tree
+unit x  =  Node Leaf x Leaf
+
+nil :: Tree -> Bool
+nil Leaf  =  True
+nil _     =  False
+
+left :: Tree -> Tree
+left (Node l _ _)  =  l
+
+right :: Tree -> Tree
+right (Node _ _ r)  =  r
+
+valu :: Tree -> Int
+valu (Node _ x _)  =  x
+
+
+leftmost :: Tree -> Int
+leftmost (Node l x _)  =  if nil l then x else leftmost (left l)
+
+rightmost :: Tree -> Int
+rightmost (Node _ x r)  =  if nil r then x else rightmost (right r)
+
+height :: Tree -> Int
+height Leaf  =  -1
+height (Node l _ r)  =  1 + max (height l) (height r)
+
+size :: Tree -> Int
+size Leaf  =  0
+size (Node l _ r)  =  size l + 1 + size r
+
+-- this mem searches both sides of the tree
+mem :: Int -> Tree -> Bool
+mem _ Leaf  =  False
+mem y (Node l x r)  =  y == x || mem y l || mem y r
+
+insert :: Int -> Tree -> Tree
+insert x Leaf  =  unit x
+insert x (Node l y r)  =  case compare x y of
+  LT -> Node (insert x l) y r
+  EQ -> Node l y r
+  GT -> Node l y (insert x r)
+
+-- TODO: mem alternative for binary search trees
+
+
+instance Listable Tree where
+  tiers  =  cons0 Leaf
+        \/  cons3 Node
+
+instance Conjurable Tree where
+  conjureEquality  =  reifyEquality
+  conjureTiers     =  reifyTiers
+  conjureSubTypes x  =  conjureType (undefined :: Int)
+
+
+main :: IO ()
+main = do
+  conjure "leftmost" leftmost
+    [ value "valu" valu
+    , value "nil" nil
+    , value "left" left
+    , value "right" right
+    ]
+
+  conjure "rightmost" rightmost
+    [ value "valu" valu
+    , value "nil" nil
+    , value "left" left
+    , value "right" right
+    ]
+
+  conjureWith args{maxRecursiveCalls=2, maxSize=13} "size" size
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "nil" nil
+    , value "left" left
+    , value "right" right
+    ]
+
+  conjureWith args{maxRecursiveCalls=2, maxSize=13} "height" height
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , val (-1 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "max" (max :: Int -> Int -> Int)
+    , value "nil" nil
+    , value "left" left
+    , value "right" right
+    ]
+
+  -- out of reach performance-wise
+  conjureWith args{maxRecursiveCalls=2, maxSize=12} "mem" mem
+    [ val False
+    , value "||" (||)
+    , value "==" ((==) :: Int -> Int -> Bool)
+    , value "nil" nil
+    , value "left" left
+    , value "right" right
+    , value "valu" valu
+    ]
+
+  -- simply out of reach performance-wise (size 34)
+  conjureWith args{maxRecursiveCalls=2, maxSize=9} "insert" mem
+    [ val Leaf
+    , value "Node" Node
+    , value "left" left
+    , value "right" right
+    , value "valu" valu
+    , value "nil" nil
+    , value "unit" unit
+    , value "==" ((==) :: Int -> Int -> Bool)
+    , value "<" ((<) :: Int -> Int -> Bool)
+    , value ">" ((>) :: Int -> Int -> Bool)
+    ]
+
+
+sizeIf :: Tree -> Int
+sizeIf t  =  if nil t  -- 3
+             then 0    -- 4
+             else sizeIf (left t) + sizeIf (right t)
+             --      5     6   7  8   9      10  11
+
+heightIf :: Tree -> Int
+heightIf t  =  if nil t  -- 3
+               then -1   -- 4
+               else 1 + max (height (left t)) (height (right t))
+               --   5 6  7     8      9  10      11     12   13
+
+memIf :: Int -> Tree -> Bool
+memIf y t  =  if nil t     -- 3
+              then False   -- 4
+              else y == valu t || memIf y (left t) || memIf y (right t)
+              --   5  6   7  8  9  10  11   12  13 14  15  16   17   18
+
+insertIf :: Int -> Tree -> Tree
+insertIf x t  =  if nil t                 -- 3
+                 then unit x              -- 5
+                 else if x == valu t      -- 10
+                      then t              -- 11
+                      else if x < valu t  -- 16
+                           then Node (insert x (left t)) (valu t) (right t)  -- 25
+                           else Node (left t) (valu t) (insert x (right t))  -- 34
diff --git a/eg/tree.out b/eg/tree.out
new file mode 100644
--- /dev/null
+++ b/eg/tree.out
@@ -0,0 +1,89 @@
+leftmost :: Tree -> Int
+-- testing 60 combinations of argument values
+-- looking through 0 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 4 candidates of size 4
+-- looking through 8 candidates of size 5
+-- looking through 16 candidates of size 6
+-- looking through 32 candidates of size 7
+-- looking through 68 candidates of size 8
+-- looking through 152 candidates of size 9
+leftmost x  =  if nil (left x) then valu x else leftmost (left x)
+
+rightmost :: Tree -> Int
+-- testing 60 combinations of argument values
+-- looking through 0 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 4 candidates of size 4
+-- looking through 8 candidates of size 5
+-- looking through 16 candidates of size 6
+-- looking through 32 candidates of size 7
+-- looking through 68 candidates of size 8
+-- looking through 152 candidates of size 9
+rightmost x  =  if nil (right x) then valu x else rightmost (right x)
+
+size :: Tree -> Int
+-- testing 60 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 0 candidates of size 6
+-- looking through 9 candidates of size 7
+-- looking through 32 candidates of size 8
+-- looking through 109 candidates of size 9
+-- looking through 304 candidates of size 10
+-- looking through 817 candidates of size 11
+-- looking through 2080 candidates of size 12
+-- looking through 5165 candidates of size 13
+size x  =  if nil x then 0 else 1 + (size (left x) + size (right x))
+
+height :: Tree -> Int
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 0 candidates of size 4
+-- looking through 2 candidates of size 5
+-- looking through 0 candidates of size 6
+-- looking through 21 candidates of size 7
+-- looking through 48 candidates of size 8
+-- looking through 239 candidates of size 9
+-- looking through 656 candidates of size 10
+-- looking through 2149 candidates of size 11
+-- looking through 5704 candidates of size 12
+-- looking through 16380 candidates of size 13
+height x  =  if nil x then -1 else 1 + max (height (left x)) (height (right x))
+
+mem :: Int -> Tree -> Bool
+-- testing 60 combinations of argument values
+-- looking through 1 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 12 candidates of size 5
+-- looking through 28 candidates of size 6
+-- looking through 64 candidates of size 7
+-- looking through 156 candidates of size 8
+-- looking through 376 candidates of size 9
+-- looking through 926 candidates of size 10
+-- looking through 2280 candidates of size 11
+-- looking through 5648 candidates of size 12
+cannot conjure
+
+insert :: Int -> Tree -> Bool
+-- testing 60 combinations of argument values
+-- looking through 0 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 16 candidates of size 4
+-- looking through 36 candidates of size 5
+-- looking through 90 candidates of size 6
+-- looking through 205 candidates of size 7
+-- looking through 497 candidates of size 8
+-- looking through 1199 candidates of size 9
+cannot conjure
+
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -7,8 +7,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   bench/ill-hit.hs
 bench/longshot: \
   bench/longshot.hs \
@@ -19,8 +19,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   bench/longshot.hs
 bench/self: \
   bench/self.hs \
@@ -31,8 +31,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   bench/self.hs
 bench/take-drop: \
   bench/take-drop.hs \
@@ -43,8 +43,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   bench/take-drop.hs
 eg/arith: \
   eg/arith.hs \
@@ -55,8 +55,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/arith.hs
 eg/bools: \
   eg/bools.hs \
@@ -67,9 +67,21 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/bools.hs
+eg/count: \
+  eg/count.hs \
+  mk/toplibs
+eg/count.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
+  eg/count.hs
 eg/factorial: \
   eg/factorial.hs \
   mk/toplibs
@@ -79,8 +91,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/factorial.hs
 eg/fibonacci: \
   eg/fibonacci.hs \
@@ -91,9 +103,21 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/fibonacci.hs
+eg/gcd: \
+  eg/gcd.hs \
+  mk/toplibs
+eg/gcd.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
+  eg/gcd.hs
 eg/ints: \
   eg/ints.hs \
   mk/toplibs
@@ -103,8 +127,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/ints.hs
 eg/list: \
   eg/list.hs \
@@ -115,9 +139,21 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/list.hs
+eg/setelem: \
+  eg/setelem.hs \
+  mk/toplibs
+eg/setelem.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
+  eg/setelem.hs
 eg/spec: \
   eg/spec.hs \
   mk/toplibs
@@ -127,8 +163,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/spec.hs
 eg/tapps: \
   eg/tapps.hs \
@@ -139,17 +175,29 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   eg/tapps.hs
+eg/tree: \
+  eg/tree.hs \
+  mk/toplibs
+eg/tree.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
+  eg/tree.hs
 mk/All.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   mk/All.hs
 mk/Toplibs.o: \
   src/Conjure/Utils.hs \
@@ -157,28 +205,28 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
   src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs \
   mk/Toplibs.hs
 proto/u-conjure.o: \
   proto/u-conjure.hs
 proto/u-conjure: \
   proto/u-conjure.hs \
   mk/toplibs
+src/Conjure/Cases.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Cases.hs
 src/Conjure/Conjurable.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Expr.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
-src/Conjure/Constructors.o: \
-  src/Conjure/Utils.hs \
-  src/Conjure/Constructors.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 src/Conjure/Engine.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 src/Conjure/Expr.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Expr.hs
@@ -188,15 +236,15 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 src/Conjure/Spec.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Spec.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 src/Conjure/Utils.o: \
   src/Conjure/Utils.hs
 test/conjurable.o: \
@@ -209,8 +257,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 test/conjurable: \
   test/Test.hs \
   test/Test/ListableExpr.hs \
@@ -227,8 +275,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 test/expr: \
   test/Test.hs \
   test/Test/ListableExpr.hs \
@@ -250,8 +298,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 test/Test: \
   test/Test.hs \
   test/Test/ListableExpr.hs \
@@ -267,8 +315,8 @@
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
-  src/Conjure/Constructors.hs \
-  src/Conjure/Conjurable.hs
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Cases.hs
 test/utils: \
   test/utils.hs \
   test/Test.hs \
diff --git a/proto/u-conjure.out b/proto/u-conjure.out
new file mode 100644
--- /dev/null
+++ b/proto/u-conjure.out
@@ -0,0 +1,24 @@
+square :: Int -> Int
+square x  =  x * x
+
+add :: Int -> Int -> Int
+add x y  =  x + y
+
+factorial :: Int -> Int
+cannot conjure
+
+factorial :: Int -> Int
+factorial x  =  foldr (*) 1 (enumFromTo 1 x)
+
+second :: [Int] -> Int
+second xs  =  head (tail xs)
+
+(++) :: [Int] -> [Int] -> [Int]
+xs ++ ys  =  foldr (:) ys xs
+
+reverse :: [Int] -> [Int]
+cannot conjure
+
+reverse :: [Int] -> [Int]
+reverse xs  =  foldr (foldr (:) . unit) [] xs
+
diff --git a/src/Conjure.hs b/src/Conjure.hs
--- a/src/Conjure.hs
+++ b/src/Conjure.hs
@@ -66,8 +66,9 @@
   , conjure3With
 
 -- * When using custom types
-  , Conjurable (conjureEquality, conjureTiers)
+  , Conjurable (conjureEquality, conjureTiers, conjureSubTypes)
   , reifyEquality, reifyTiers
+  , conjureType
 
 -- * Pure interfaces
   , conjpure
diff --git a/src/Conjure/Cases.hs b/src/Conjure/Cases.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Cases.hs
@@ -0,0 +1,122 @@
+-- |
+-- Module      : Conjure.Cases
+-- Copyright   : (c) 2021 Rudy Matela
+-- License     : 3-Clause BSD  (see the file LICENSE)
+-- Maintainer  : Rudy Matela <rudy@matela.com.br>
+--
+-- This module is part of 'Conjure'.
+--
+-- This module defines the 'Cases' typeclass
+-- that allows listing cases of a type
+-- encoded as 'Expr's
+--
+-- You are probably better off importing "Conjure".
+{-# Language DeriveDataTypeable, StandaloneDeriving #-} -- for GHC < 7.10
+module Conjure.Cases
+  ( Cases (..)
+  , Fxpr
+  , sumFxpr
+  , factFxpr
+  , nullFxpr
+  , isZeroFxpr
+  )
+where
+
+import Conjure.Utils
+import Data.Express
+import Data.Express.Express
+import Data.Express.Fixtures
+import Data.Dynamic
+import Data.Typeable (Typeable)
+
+type Fxpr  =  (Expr, Cxpr)
+type Cxpr  =  [([Expr],Expr)]
+
+sumFxpr :: Fxpr
+sumFxpr  =  var "sum" (undefined :: [Int] -> Int) =-
+  [ [nil]           =-  zero
+  , [(xx -:- xxs)]  =-  xx -+- (var "recurse" (undefined :: [Int] -> Int) :$ xxs)
+  ]
+  where
+  (=-) = (,)
+  infixr 0 =-
+
+factFxpr :: Fxpr
+factFxpr  =  error "TODO: write me"
+
+nullFxpr :: Fxpr
+nullFxpr  =  error "TODO" =-
+  [ [nil]          =- false
+  , [(xx -:- xxs)] =- false
+  ]
+  where
+  (=-) = (,)
+  infixr 0 =-
+
+isZeroFxpr :: Fxpr
+isZeroFxpr  =  error "TODO" =-
+  [ [zero]  =- true
+  , [inc xx] =- false
+  ]
+  where
+  inc = undefined -- TODO: define me
+  (=-) = (,)
+  infixr 0 =-
+
+
+-- | Evaluates an 'Expr' using the given 'Fxpr' as definition
+--   when a recursive call is found.
+fxprToDynamic :: Int -> Fxpr -> Expr -> Maybe Dynamic
+fxprToDynamic  =  undefined
+
+
+class Express a => Cases a where
+  cases :: a -> [Expr]
+
+instance Cases () where
+  cases _  =  [val ()]
+
+instance Cases Bool where
+  cases _  =  [val False, val True]
+
+instance Cases Int where
+  cases x  =  [val (0 -: x), hole x]
+
+instance Cases Integer where
+  cases x  =  [val (0 -: x), hole x]
+
+instance Cases Char where
+  cases _  =  []
+
+instance Express a => Cases [a] where
+  cases xs  =  [ val ([] -: xs)
+               , value ":" ((:) ->>: xs) :$ hole x :$ hole xs
+               ]
+    where
+    x  =  head xs
+
+instance (Express a, Express b) => Cases (a,b) where
+  cases xy  =  [value "," ((,) ->>: xy) :$ hole x :$ hole y]
+    where
+    (x,y) = (undefined,undefined) -: xy
+
+instance (Express a, Express b, Express c) => Cases (a,b,c) where
+  cases xyz  =  [value ",," ((,,) ->>>: xyz) :$ hole x :$ hole y :$ hole z]
+    where
+    (x,y,z) = (undefined,undefined,undefined) -: xyz
+
+instance Express a => Cases (Maybe a) where
+  cases mx  =  [ value "Nothing" (Nothing -: mx)
+               , value "Just" (Just ->: mx) :$ hole x
+               ]
+    where
+    x  =  Just undefined -: mx
+
+
+instance (Express a, Express b) => Cases (Either a b) where
+  cases exy  =  [ value "Left" (Left ->: exy) :$ hole x
+                , value "Right" (Right ->: exy) :$ hole y
+                ]
+    where
+    x  =  Left undefined -: exy
+    y  =  Right undefined -: exy
diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs
--- a/src/Conjure/Conjurable.hs
+++ b/src/Conjure/Conjurable.hs
@@ -10,7 +10,6 @@
 -- and utilities involving it.
 --
 -- You are probably better off importing "Conjure".
-{-# Language DeriveDataTypeable, StandaloneDeriving #-} -- for GHC < 7.10
 module Conjure.Conjurable
   ( Reification1
   , Reification
@@ -34,7 +33,7 @@
 import Test.LeanCheck.Utils
 import Test.LeanCheck.Error (errorToFalse)
 import Conjure.Expr hiding (application)
-import Conjure.Constructors
+import Conjure.Cases
 import Test.Speculate.Expr
 import Data.Functor ((<$>))
 import Control.Applicative ((<*>))
@@ -420,13 +419,6 @@
 instance Conjurable F where
   conjureEquality  =  reifyEquality
   conjureTiers     =  reifyTiers
-
-deriving instance Typeable A -- for GHC < 7.10
-deriving instance Typeable B -- for GHC < 7.10
-deriving instance Typeable C -- for GHC < 7.10
-deriving instance Typeable D -- for GHC < 7.10
-deriving instance Typeable E -- for GHC < 7.10
-deriving instance Typeable F -- for GHC < 7.10
 
 
 -- Conjurable tuples --
diff --git a/src/Conjure/Constructors.hs b/src/Conjure/Constructors.hs
deleted file mode 100644
--- a/src/Conjure/Constructors.hs
+++ /dev/null
@@ -1,165 +0,0 @@
--- |
--- Module      : Conjure.Constructors
--- Copyright   : (c) 2021 Rudy Matela
--- License     : 3-Clause BSD  (see the file LICENSE)
--- Maintainer  : Rudy Matela <rudy@matela.com.br>
---
--- This module is part of 'Conjure'.
---
--- This module defines the 'Constructors' typeclass
--- that allows listing constructors of a type
--- encoded as 'Expr's
---
--- You are probably better off importing "Conjure".
-{-# Language DeriveDataTypeable, StandaloneDeriving #-} -- for GHC < 7.10
-module Conjure.Constructors
-  ( Constructors (..)
-  , Fxpr
-  , Fxpress (..)
-  , sumFxpr
-  , factFxpr
-  , nullFxpr
-  , isZeroFxpr
-  )
-where
-
-import Conjure.Utils
-import Data.Express
-import Data.Express.Express
-import Data.Express.Fixtures
-import Data.Typeable (Typeable)
-
-type Fxpr  =  [([Expr],Expr)]
-
-sumFxpr :: Fxpr
-sumFxpr  =
-  [ [nil]           =-  zero
-  , [(xx -:- xxs)]  =-  xx -+- (var "recurse" (undefined :: [Int] -> Int) :$ xxs)
-  ]
-  where
-  (=-) = (,)
-  infixr 0 =-
-
-factFxpr :: Fxpr
-factFxpr  =  undefined
-
-nullFxpr :: Fxpr
-nullFxpr  =
-  [ [nil]          =- false
-  , [(xx -:- xxs)] =- false
-  ]
-  where
-  (=-) = (,)
-  infixr 0 =-
-
-isZeroFxpr :: Fxpr
-isZeroFxpr  =
-  [ [zero]  =- true
-  , [inc xx] =- false
-  ]
-  where
-  inc = undefined -- TODO: define me
-  (=-) = (,)
-  infixr 0 =-
-
-
-class Typeable a => Fxpress a where
-  fvl :: Fxpr -> a
-  fvl (([],e):_)  =  evl e
-  fvl _           =  error "fvl: incomplete pattern match"
-
-instance Fxpress ()
-instance Fxpress Int
-instance Fxpress Bool
-instance Fxpress Char
-instance Fxpress a => Fxpress [a]
-instance Fxpress a => Fxpress (Maybe a)
-instance (Fxpress a, Fxpress b) => Fxpress (Either a b)
-
-instance (Constructors a, Fxpress b) => Fxpress (a -> b) where
-  fvl cs x  =  fvl [ (ps,exp //- bs)
-                   | (p:ps,exp) <- cs
-                   , bs <- maybeToList (match (expr1 x) p)
-                   ]
--- TODO: add support for recursion
-
-
-class Express a => Constructors a where
-  expr1 :: a -> Expr
-  constructors :: a -> [Expr]
-
-instance Constructors () where
-  expr1  =  val
-  constructors _  =  [val ()]
-
-instance Constructors Bool where
-  expr1  =  val
-  constructors _  =  [val False, val True]
-
-constructorsNum :: (Num a, Express a) => a -> [Expr]
-constructorsNum x  =  [ hole x -- <= 0 -- val (0 -: x)
-                      , value "inc" ((+1) ->: x) :$ hole x
-                      ]
-
-expr1Num :: (Ord a, Num a, Express a) => a -> Expr
-expr1Num x
-  | x <= 0     =  val x
-  | otherwise  =  value "inc" ((+1) ->: x) :$ val (x-1)
-
-instance Constructors Int where
-  expr1  =  expr1Num
-  constructors  =  constructorsNum
-
-instance Constructors Integer where
-  expr1  =  expr1Num
-  constructors  =  constructorsNum
-
-instance Constructors Char where
-  expr1  =  val
-  constructors _  =  []
-
-instance Express a => Constructors [a] where
-  expr1 xs  =  case xs of
-               [] -> val xs
-               (y:ys) -> value ":" ((:) ->>: xs) :$ val y :$ val ys
-  constructors xs  =  [ val ([] -: xs)
-                      , value ":" ((:) ->>: xs) :$ hole x :$ hole xs
-                      ]
-    where
-    x  =  head xs
-
-
-instance (Express a, Express b) => Constructors (a,b) where
-  expr1 (x,y)  =  value "," ((,) ->>: (x,y))
-               :$ val x :$ val y
-  constructors xy  =  [value "," ((,) ->>: xy) :$ hole x :$ hole y]
-    where
-    (x,y) = (undefined,undefined) -: xy
-
-instance (Express a, Express b, Express c) => Constructors (a,b,c) where
-  expr1 (x,y,z)  =  value ",," ((,,) ->>>: (x,y,z))
-                 :$ val x :$ val y :$ val z
-
-  constructors xyz  =  [value ",," ((,,) ->>>: xyz) :$ hole x :$ hole y :$ hole z]
-    where
-    (x,y,z) = (undefined,undefined,undefined) -: xyz
-
-instance Express a => Constructors (Maybe a) where
-  expr1 mx@Nothing   =  value "Nothing" (Nothing -: mx)
-  expr1 mx@(Just x)  =  value "Just"    (Just   ->: mx) :$ val x
-  constructors mx  =  [ value "Nothing" (Nothing -: mx)
-                      , value "Just" (Just ->: mx) :$ hole x
-                      ]
-    where
-    x  =  Just undefined -: mx
-
-
-instance (Express a, Express b) => Constructors (Either a b) where
-  expr1 lx@(Left x)   =  value "Left"  (Left  ->: lx) :$ val x
-  expr1 ry@(Right y)  =  value "Right" (Right ->: ry) :$ val y
-  constructors exy  =  [ value "Left" (Left ->: exy) :$ hole x
-                       , value "Right" (Right ->: exy) :$ hole y
-                       ]
-    where
-    x  =  Left undefined -: exy
-    y  =  Right undefined -: exy
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -36,7 +36,7 @@
 import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
 
 import Test.Speculate.Reason (Thy, rules, equations, canReduceTo, printThy)
-import Test.Speculate.Engine (theoryFromAtoms, groundBinds)
+import Test.Speculate.Engine (theoryFromAtoms, groundBinds, boolTy)
 
 import Conjure.Expr
 import Conjure.Conjurable
@@ -131,18 +131,18 @@
   putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"
   pr 1 rs
   where
-  pr n []  =  putStrLn $ "cannot conjure"
-  pr n ((is,cs,es):rs)  =  do
+  pr n []  =  putStrLn $ "cannot conjure\n"
+  pr n ((is,cs):rs)  =  do
     putStrLn $ "-- looking through "
             ++ show (length cs)
             ++ " candidates of size " ++ show n
-    -- when (n<=6) $ putStrLn $ unlines $ map show es
+    -- when (n<=7) $ putStrLn $ unlines $ map show es
     case is of
       []     ->  pr (n+1) rs
       (i:_)  ->  do putStrLn $ showEq i
                     putStrLn ""
-  rs  =  zip3 iss css ess
-  (iss, css, ess, ts)  =  conjpureWith args nm f es
+  rs  =  zip iss css
+  (iss, css, ts)  =  conjpureWith args nm f es
 
 
 -- | Like 'conjure' but in the pure world.
@@ -153,21 +153,20 @@
 -- 2. tiers of candidate bodies (right type)
 -- 3. tiers of candidate expressions (any type)
 -- 4. a list of tests
-conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
+conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
 conjpure =  conjpureWith args
 
 
 -- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
-conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
-conjpureWith Args{..} nm f es  =  (implementationsT, candidatesT, allCandidatesT, tests)
+conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
+conjpureWith Args{..} nm f es  =  (implementationsT, candidatesT, tests)
   where
   tests  =  [ffxx //- bs | bs <- dbss]
   implementationsT  =  mapT (vffxx -==-) $ filterT implements candidatesT
   implements e  =  apparentlyTerminates rrff e
-                && requal (vffxx,e) ffxx e
-  candidatesT  =  filterT (\e -> typ e == typ ffxx) allCandidatesT
-  allCandidatesT  =  take maxSize
-                  $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===) es
+                && requal (vffxx,e) ffxx vffxx
+  candidatesT  =  take maxSize
+               $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===) es
   ffxx   =  conjureApplication nm f
   vffxx  =  conjureVarApplication nm f
   (rrff:xxs)  =  unfoldApp vffxx
@@ -197,15 +196,16 @@
                -> [[Expr]]
 candidateExprs nm f sz mc (===) es  =  as \/ ts
   where
-  ts  =  filterT keepIf
-      $  foldAppProducts (conjureIf f) [cs, as, rs]
-      \/ foldAppProducts (conjureIf f) [cs, rs, as]
+  ts | typ efxs == boolTy  =  foldAppProducts andE [cs, rs]
+                           \/ foldAppProducts orE  [cs, rs]
+     | otherwise           =  filterT keepIf
+                           $  foldAppProducts (conjureIf f) [cs, as, rs]
+                           \/ foldAppProducts (conjureIf f) [cs, rs, as]
   cs  =  filterT (`notElem` [val False, val True])
       $  forN (hole (undefined :: Bool))
   as  =  forN efxs
   rs  =  forR efxs
   forN h  =  enumerateAppsFor h keep [exs ++ es]
-  forD h  =  enumerateAppsFor h (const True) [exs ++ ds]
   forR h  =  filterT (\e -> (ef `elem`) (vars e))
           $  enumerateAppsFor h keep $ [exs ++ es] \/ recs
   efxs  =  conjureVarApplication nm f
@@ -215,8 +215,81 @@
   thy  =  theoryFromAtoms (===) sz . (:[]) . nub
        $  conjureHoles f ++ [val False, val True] ++ es
   ds  =  map snd $ deconstructors f 60 es
-  recs  =  filterT (efxs /=)
-        $  foldAppProducts ef [forD h | h <- conjureArgumentHoles f]
+  recs  =  filterT (descends (`elem` ds) efxs)
+        $  foldAppProducts ef [forN h | h <- conjureArgumentHoles f]
+
+-- | Returns whether the given recursive call
+--   deconstructs one of its arguments.
+--
+-- > > deconstructs1 ... (factorial' (dec' xx))
+-- > True
+--
+-- > > deconstructs1 ... (factorial' (xx -+- one))
+-- > False
+--
+-- > > deconstructs1 ... (xxs -++- yys)
+-- > False
+--
+-- > > deconstructs1 ... (xxs -++- tail' yys)
+-- > True
+--
+-- > > deconstructs1 ... (zero-:-xxs -++- tail' yys)
+-- > True
+--
+-- 'deconstructs1' implies 'descends'.
+deconstructs1 :: (Expr -> Bool) -> Expr -> Expr -> Bool
+deconstructs1 isDec _ e  =  any isDeconstruction exs
+  where
+  (ef:exs)  =  unfoldApp e
+  isDeconstruction e  =  not (null cs) && all isDec cs
+    where
+    cs  =  consts e
+
+-- | Returns whether a non-empty subset of arguments
+--   descends arguments by deconstruction.
+--
+-- > > descends isDec (xxs -++- yys) (xxs -++- tail' yys)
+-- > True
+--
+-- > > descends isDec (xxs -++- yys) (xxs -++- yys)
+-- > False
+--
+-- > > descends isDec (xxs -++- yys) (head' xxs -:- tail xxs  -++-  head' yys -:- tail yys)
+-- > False
+
+-- > > descends isDec (xxs -\/- yys) (yys -\/- tail' xxs)
+-- > True
+--
+-- The following are not so obvious:
+--
+-- > > descends isDec (xxs -++- yys) (tail' yys -++- yys)
+-- > False
+--
+-- > > descends isDec (xxs -++- yys) (xx-:-xxs -++- tail' yys)
+-- > True
+--
+-- For all possible sets of arguments (2^n - 1 elements: 1 3 7 15 31),
+-- see if any projects the same variables while only using deconstructions
+-- and where there is at least a single deconstruction.
+descends :: (Expr -> Bool) -> Expr -> Expr -> Bool
+descends isDec e' e  =  any d1 ss
+  where
+  d1 exys  =  nubVars (foldApp exs) == nubVars (foldApp eys)
+           && all isNotConstruction eys
+           && any isDeconstruction eys
+    where
+    exs  =  map fst exys
+    eys  =  map snd exys
+  ss  =  init $ sets exys
+  exys  =  zip exs eys
+  (_:exs)  =  unfoldApp e'
+  (_:eys)  =  unfoldApp e
+  isDeconstruction e  =  not (null cs) && all isDec cs
+    where
+    cs  =  consts e
+  isNotConstruction e  =  all isDec cs
+    where
+    cs  =  consts e
 
 -- | Example:
 --
diff --git a/src/Conjure/Expr.hs b/src/Conjure/Expr.hs
--- a/src/Conjure/Expr.hs
+++ b/src/Conjure/Expr.hs
@@ -341,24 +341,42 @@
 isDeconstructionE es ez ed  =  isDeconstruction es (eval False . (ez :$)) (ed :$)
 
 recursiveToDynamic :: (Expr,Expr) -> Int -> Expr -> Maybe Dynamic
-recursiveToDynamic (efxs, ebody) n  =  fmap snd . re n
+recursiveToDynamic (efxs, ebody) n  =  fmap (\(_,_,d) -> d) . re (n * size ebody) n
   where
   (ef':exs')  =  unfoldApp efxs
-  re :: Int -> Expr -> Maybe (Int, Dynamic)
-  re n _  | n <= 0  =  error "recursiveToDynamic: recursion limit reached"
-  re n (Value "if" _ :$ ec :$ ex :$ ey)  =  case evaluate ec of
+
+  rev :: Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
+  rev m n e  =  case re m n e of
+                Nothing    -> Nothing
+                Just (m,n,d) -> case fromDynamic d of
+                                Nothing -> Nothing
+                                Just x  -> Just (m, n, x)
+
+  re :: Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
+  re m n _  | n <= 0  =  error "recursiveToDynamic: recursion limit reached"
+  re m n _  | m <= 0  =  error "recursiveToDynamic: evaluation limit reached"
+  re m n (Value "if" _ :$ ec :$ ex :$ ey)  =  case rev m n ec of
     Nothing    -> Nothing
-    Just True  -> re n ex
-    Just False -> re n ey
-  re n e  =  case unfoldApp e of
+    Just (m,n,True)  -> re m n ex
+    Just (m,n,False) -> re m n ey
+  re m n (Value "||" _ :$ ep :$ eq)  =  case rev m n ep of
+    Nothing        -> Nothing
+    Just (m,n,True)  -> (m,n,) <$> toDynamic (val True)
+    Just (m,n,False) -> re m n eq
+  re m n (Value "&&" _ :$ ep :$ eq)  =  case rev m n ep of
+    Nothing    -> Nothing
+    Just (m,n,True)  -> re m n eq
+    Just (m,n,False) -> (m,n,) <$> toDynamic (val False)
+  re m n e  =  case unfoldApp e of
     [] -> error "recursiveToDynamic: empty application unfold"  -- should never happen
-    [e] -> (n,) <$> toDynamic e
-    (ef:exs) | ef == ef' -> re (n-1) $ ebody //- zip exs' exs
-             | otherwise -> foldl ($$) (re n ef) exs
-  Just (n,d1) $$ e2  =  case re n e2 of
-                        Nothing -> Nothing
-                        Just (n', d2) -> (n',) <$> dynApply d1 d2
-  _ $$ _             =  Nothing
+    [e] -> (m-1,n,) <$> toDynamic e
+    (ef:exs) | ef == ef' -> re m (n-1) $ ebody //- zip exs' exs
+             | otherwise -> foldl ($$) (re m n ef) exs
+
+  Just (m,n,d1) $$ e2  =  case re m n e2 of
+                          Nothing -> Nothing
+                          Just (m', n', d2) -> (m',n',) <$> dynApply d1 d2
+  _ $$ _               =  Nothing
 
 revaluate :: Typeable a => (Expr,Expr) -> Int -> Expr -> Maybe a
 revaluate dfn n e  =  recursiveToDynamic dfn n e >>= fromDynamic
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
--- a/src/Conjure/Utils.hs
+++ b/src/Conjure/Utils.hs
@@ -31,6 +31,7 @@
   , isDeconstruction
   , idIO
   , mapHead
+  , sets
   )
 where
 
@@ -111,3 +112,9 @@
 
 mapHead :: (a -> a) -> [a] -> [a]
 mapHead f (x:xs)  =  f x : xs
+
+sets :: [a] -> [[a]]
+sets []  =  [[]]
+sets (x:xs)  =  map (x:) ss ++ ss
+  where
+  ss  =  sets xs
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -9,6 +9,6 @@
 - .
 
 extra-deps:
-- leancheck-0.9.6
-- speculate-0.4.6
-- express-0.1.12
+- leancheck-0.9.10
+- speculate-0.4.8
+- express-0.1.14
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -20,7 +20,7 @@
 where
 
 import System.Exit (exitFailure)
-import System.Environment (getArgs)
+import System.Environment (getArgs, getProgName)
 
 import Test.LeanCheck
 import Test.LeanCheck.Utils
@@ -31,11 +31,11 @@
 import Conjure.Expr hiding (delete, insert)
 import Conjure.Conjurable
 
-reportTests :: [Bool] -> IO ()
-reportTests tests =
+reportTests :: String -> [Bool] -> IO ()
+reportTests s tests = do
   case elemIndices False tests of
-    [] -> putStrLn "Tests passed!"
-    is -> do putStrLn ("Failed tests:" ++ show is)
+    [] -> putStrLn $ s ++ ": tests passed"
+    is -> do putStrLn (s ++ ": failed tests: " ++ show is)
              exitFailure
 
 getMaxTestsFromArgs :: Int -> IO Int
@@ -47,8 +47,9 @@
 
 mainTest :: (Int -> [Bool]) -> Int -> IO ()
 mainTest tests n' = do
+  pn <- getProgName
   n <- getMaxTestsFromArgs n'
-  reportTests (tests n)
+  reportTests pn (tests n)
 
 printLines :: Show a => [a] -> IO ()
 printLines = putStrLn . unlines . map show
diff --git a/test/model/bench/ill-hit.out b/test/model/bench/ill-hit.out
deleted file mode 100644
--- a/test/model/bench/ill-hit.out
+++ /dev/null
@@ -1,42 +0,0 @@
-sum :: [Int] -> Int
--- testing 4 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
--- looking through 5 candidates of size 5
--- looking through 5 candidates of size 6
--- looking through 15 candidates of size 7
--- looking through 27 candidates of size 8
--- looking through 53 candidates of size 9
--- looking through 101 candidates of size 10
-sum xs  =  if null xs then 0 else head xs + sum (tail xs)
-
-sum :: [Int] -> Int
--- testing 6 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
--- looking through 5 candidates of size 5
--- looking through 5 candidates of size 6
--- looking through 15 candidates of size 7
--- looking through 27 candidates of size 8
--- looking through 53 candidates of size 9
--- looking through 101 candidates of size 10
-sum xs  =  if null xs then 0 else head xs + sum (tail xs)
-
-sum :: [Int] -> Int
--- testing 6 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
--- looking through 5 candidates of size 5
--- looking through 5 candidates of size 6
--- looking through 15 candidates of size 7
--- looking through 27 candidates of size 8
--- looking through 53 candidates of size 9
--- looking through 101 candidates of size 10
-sum xs  =  if null xs then 0 else head xs + sum (tail xs)
-
diff --git a/test/model/bench/longshot.out b/test/model/bench/longshot.out
deleted file mode 100644
--- a/test/model/bench/longshot.out
+++ /dev/null
@@ -1,37 +0,0 @@
-qsort :: [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 3 candidates of size 3
--- looking through 11 candidates of size 4
--- looking through 28 candidates of size 5
--- looking through 72 candidates of size 6
--- looking through 207 candidates of size 7
--- looking through 611 candidates of size 8
--- looking through 1779 candidates of size 9
--- looking through 5301 candidates of size 10
--- looking through 16103 candidates of size 11
--- looking through 49113 candidates of size 12
-cannot conjure
-pow :: Int -> Int -> Int
--- testing 5 combinations of argument values
--- looking through 4 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 13 candidates of size 3
--- looking through 20 candidates of size 4
--- looking through 80 candidates of size 5
--- looking through 172 candidates of size 6
--- looking through 614 candidates of size 7
--- looking through 1675 candidates of size 8
-cannot conjure
-pow :: Int -> Int -> Int
--- testing 5 combinations of argument values
--- looking through 4 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 15 candidates of size 3
--- looking through 26 candidates of size 4
--- looking through 111 candidates of size 5
--- looking through 307 candidates of size 6
--- looking through 1122 candidates of size 7
--- looking through 3727 candidates of size 8
-cannot conjure
diff --git a/test/model/bench/self.out b/test/model/bench/self.out
deleted file mode 100644
--- a/test/model/bench/self.out
+++ /dev/null
@@ -1,27 +0,0 @@
-(?) :: Int -> Int -> Int
--- testing 60 combinations of argument values
--- looking through 4 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 32 candidates of size 3
-x ? y  =  x + y
-
-(?) :: Int -> Int -> Int
--- testing 60 combinations of argument values
--- looking through 4 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 32 candidates of size 3
-x ? y  =  x * y
-
-i :: Int -> Int
--- testing 60 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 18 candidates of size 3
-i x  =  x + 1
-
-d :: Int -> Int
--- testing 60 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 18 candidates of size 3
-cannot conjure
diff --git a/test/model/bench/take-drop.out b/test/model/bench/take-drop.out
deleted file mode 100644
--- a/test/model/bench/take-drop.out
+++ /dev/null
@@ -1,37 +0,0 @@
-drop :: Int -> [A] -> [A]
--- testing 60 combinations of argument values
--- looking through 1 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 1 candidates of size 3
--- looking through 1 candidates of size 4
--- looking through 1 candidates of size 5
--- looking through 1 candidates of size 6
--- looking through 1 candidates of size 7
--- looking through 5 candidates of size 8
--- looking through 21 candidates of size 9
--- looking through 60 candidates of size 10
--- looking through 136 candidates of size 11
--- looking through 288 candidates of size 12
--- looking through 601 candidates of size 13
-drop x y  =  if null y || x == 0 then y else drop (dec x) (tail y)
-
-take :: Int -> [A] -> [A]
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 6 candidates of size 4
--- looking through 10 candidates of size 5
--- looking through 14 candidates of size 6
--- looking through 26 candidates of size 7
--- looking through 54 candidates of size 8
--- looking through 122 candidates of size 9
--- looking through 280 candidates of size 10
--- looking through 636 candidates of size 11
--- looking through 1512 candidates of size 12
--- looking through 3618 candidates of size 13
--- looking through 8400 candidates of size 14
--- looking through 19152 candidates of size 15
--- looking through 43184 candidates of size 16
-take x y  =  if null y || x == 0 then [] else head y:take (dec x) (tail y)
-
diff --git a/test/model/eg/arith.out b/test/model/eg/arith.out
deleted file mode 100644
--- a/test/model/eg/arith.out
+++ /dev/null
@@ -1,32 +0,0 @@
-double :: Int -> Int
--- testing 4 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 5 candidates of size 3
-double x  =  x + x
-
-add :: Int -> Int -> Int
--- testing 4 combinations of argument values
--- looking through 4 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 13 candidates of size 3
-add x y  =  x + y
-
-square :: Int -> Int
--- testing 3 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 5 candidates of size 3
-square x  =  x * x
-
-tnpo :: Int -> Int
--- testing 3 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 5 candidates of size 3
--- looking through 0 candidates of size 4
--- looking through 13 candidates of size 5
--- looking through 0 candidates of size 6
--- looking through 42 candidates of size 7
-tnpo x  =  x + (x + (x + 1))
-
diff --git a/test/model/eg/bools.out b/test/model/eg/bools.out
deleted file mode 100644
--- a/test/model/eg/bools.out
+++ /dev/null
@@ -1,44 +0,0 @@
-and :: [Bool] -> Bool
--- testing 14 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 4 candidates of size 4
--- looking through 6 candidates of size 5
--- looking through 15 candidates of size 6
--- looking through 37 candidates of size 7
--- looking through 88 candidates of size 8
--- looking through 200 candidates of size 9
--- looking through 464 candidates of size 10
-and ps  =  if null ps then True else head ps && and (tail ps)
-
-or :: [Bool] -> Bool
--- testing 14 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 4 candidates of size 4
--- looking through 6 candidates of size 5
--- looking through 15 candidates of size 6
--- looking through 37 candidates of size 7
--- looking through 88 candidates of size 8
--- looking through 200 candidates of size 9
--- looking through 464 candidates of size 10
-or ps  =  if null ps then False else head ps || or (tail ps)
-
-and :: [Bool] -> Bool
--- testing 14 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 6 candidates of size 4
-and ps  =  foldr (&&) True ps
-
-or :: [Bool] -> Bool
--- testing 14 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 6 candidates of size 4
-or ps  =  foldr (||) False ps
-
diff --git a/test/model/eg/factorial.out b/test/model/eg/factorial.out
deleted file mode 100644
--- a/test/model/eg/factorial.out
+++ /dev/null
@@ -1,22 +0,0 @@
-factorial :: Int -> Int
--- testing 6 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 0 candidates of size 3
--- looking through 2 candidates of size 4
-factorial n  =  product (enumFromTo 1 n)
-
-factorial :: Int -> Int
--- testing 6 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 5 candidates of size 3
--- looking through 6 candidates of size 4
--- looking through 20 candidates of size 5
--- looking through 27 candidates of size 6
--- looking through 87 candidates of size 7
--- looking through 167 candidates of size 8
--- looking through 421 candidates of size 9
--- looking through 968 candidates of size 10
-factorial n  =  if n == 0 then 1 else n * factorial (dec n)
-
diff --git a/test/model/eg/fibonacci.out b/test/model/eg/fibonacci.out
deleted file mode 100644
--- a/test/model/eg/fibonacci.out
+++ /dev/null
@@ -1,17 +0,0 @@
-fibonacci :: Int -> Int
--- testing 8 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 6 candidates of size 3
--- looking through 1 candidates of size 4
--- looking through 11 candidates of size 5
--- looking through 5 candidates of size 6
--- looking through 27 candidates of size 7
--- looking through 20 candidates of size 8
--- looking through 95 candidates of size 9
--- looking through 148 candidates of size 10
--- looking through 431 candidates of size 11
--- looking through 925 candidates of size 12
--- looking through 2377 candidates of size 13
-fibonacci n  =  if n <= 1 then 1 else fibonacci (dec n) + fibonacci (dec (dec n))
-
diff --git a/test/model/eg/ints.out b/test/model/eg/ints.out
deleted file mode 100644
--- a/test/model/eg/ints.out
+++ /dev/null
@@ -1,59 +0,0 @@
-second :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
-second xs  =  head (tail xs)
-
-third :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
-third xs  =  head (tail (tail xs))
-
-sum :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
--- looking through 5 candidates of size 5
--- looking through 5 candidates of size 6
--- looking through 15 candidates of size 7
--- looking through 27 candidates of size 8
--- looking through 53 candidates of size 9
--- looking through 101 candidates of size 10
-sum xs  =  if null xs then 0 else head xs + sum (tail xs)
-
-product :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
--- looking through 5 candidates of size 5
--- looking through 5 candidates of size 6
--- looking through 15 candidates of size 7
--- looking through 27 candidates of size 8
--- looking through 53 candidates of size 9
--- looking through 101 candidates of size 10
-product xs  =  if null xs then 1 else head xs * product (tail xs)
-
-sum :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 5 candidates of size 4
-sum xs  =  foldr (+) 0 xs
-
-product :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 5 candidates of size 4
-product xs  =  foldr (*) 1 xs
-
diff --git a/test/model/eg/list.out b/test/model/eg/list.out
deleted file mode 100644
--- a/test/model/eg/list.out
+++ /dev/null
@@ -1,109 +0,0 @@
-length :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 1 candidates of size 3
--- looking through 0 candidates of size 4
--- looking through 1 candidates of size 5
--- looking through 0 candidates of size 6
--- looking through 5 candidates of size 7
--- looking through 8 candidates of size 8
--- looking through 19 candidates of size 9
-length xs  =  if null xs then 0 else 1 + length (tail xs)
-
-reverse :: [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 5 candidates of size 3
--- looking through 9 candidates of size 4
--- looking through 23 candidates of size 5
--- looking through 57 candidates of size 6
--- looking through 147 candidates of size 7
--- looking through 381 candidates of size 8
--- looking through 1014 candidates of size 9
--- looking through 2736 candidates of size 10
--- looking through 7447 candidates of size 11
-reverse xs  =  if null xs then xs else reverse (tail xs) ++ unit (head xs)
-
-sort :: [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 6 candidates of size 4
--- looking through 11 candidates of size 5
--- looking through 21 candidates of size 6
--- looking through 49 candidates of size 7
--- looking through 119 candidates of size 8
--- looking through 272 candidates of size 9
--- looking through 625 candidates of size 10
-sort xs  =  if null xs then xs else insert (head xs) (sort (tail xs))
-
-(++) :: [Int] -> [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 3 candidates of size 3
--- looking through 12 candidates of size 4
--- looking through 21 candidates of size 5
--- looking through 30 candidates of size 6
--- looking through 102 candidates of size 7
--- looking through 351 candidates of size 8
--- looking through 969 candidates of size 9
--- looking through 2625 candidates of size 10
--- looking through 7086 candidates of size 11
-xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
-
-length :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 1 candidates of size 3
--- looking through 2 candidates of size 4
--- looking through 1 candidates of size 5
--- looking through 7 candidates of size 6
-length xs  =  foldr (const (1 +)) 0 xs
-
-reverse :: [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 1 candidates of size 3
--- looking through 0 candidates of size 4
--- looking through 1 candidates of size 5
--- looking through 8 candidates of size 6
--- looking through 13 candidates of size 7
-reverse xs  =  foldr (flip (++) . unit) [] xs
-
-sort :: [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 0 candidates of size 3
--- looking through 2 candidates of size 4
-sort xs  =  foldr insert [] xs
-
-(++) :: [Int] -> [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 0 candidates of size 2
--- looking through 0 candidates of size 3
--- looking through 4 candidates of size 4
-xs ++ ys  =  foldr (:) ys xs
-
-(\/) :: [Int] -> [Int] -> [Int]
--- testing 60 combinations of argument values
--- looking through 3 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 3 candidates of size 3
--- looking through 12 candidates of size 4
--- looking through 21 candidates of size 5
--- looking through 30 candidates of size 6
--- looking through 102 candidates of size 7
--- looking through 351 candidates of size 8
--- looking through 969 candidates of size 9
--- looking through 2625 candidates of size 10
--- looking through 7086 candidates of size 11
-xs \/ ys  =  if null xs then xs else head xs:ys \/ tail xs
-
diff --git a/test/model/eg/spec.out b/test/model/eg/spec.out
deleted file mode 100644
--- a/test/model/eg/spec.out
+++ /dev/null
@@ -1,29 +0,0 @@
-sum :: [Int] -> Int
--- testing 3 combinations of argument values
--- looking through 1 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 1 candidates of size 3
--- looking through 1 candidates of size 4
--- looking through 2 candidates of size 5
--- looking through 2 candidates of size 6
--- looking through 5 candidates of size 7
--- looking through 10 candidates of size 8
--- looking through 17 candidates of size 9
--- looking through 28 candidates of size 10
-sum xs  =  if null xs then 0 else head xs + sum (tail xs)
-
-(++) :: [Int] -> [Int] -> [Int]
--- testing 3 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 6 candidates of size 4
--- looking through 10 candidates of size 5
--- looking through 14 candidates of size 6
--- looking through 50 candidates of size 7
--- looking through 182 candidates of size 8
--- looking through 506 candidates of size 9
--- looking through 1310 candidates of size 10
--- looking through 3298 candidates of size 11
-xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
-
diff --git a/test/model/eg/tapps.out b/test/model/eg/tapps.out
deleted file mode 100644
--- a/test/model/eg/tapps.out
+++ /dev/null
@@ -1,30 +0,0 @@
-third :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
-third xs  =  head (tail (tail xs))
-
-product :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 2 candidates of size 4
--- looking through 5 candidates of size 5
--- looking through 5 candidates of size 6
--- looking through 15 candidates of size 7
--- looking through 27 candidates of size 8
--- looking through 53 candidates of size 9
--- looking through 101 candidates of size 10
-product xs  =  if null xs then 1 else head xs * product (tail xs)
-
-product :: [Int] -> Int
--- testing 60 combinations of argument values
--- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 2 candidates of size 3
--- looking through 5 candidates of size 4
-product xs  =  foldr (*) 1 xs
-
diff --git a/test/model/proto/u-conjure.out b/test/model/proto/u-conjure.out
deleted file mode 100644
--- a/test/model/proto/u-conjure.out
+++ /dev/null
@@ -1,24 +0,0 @@
-square :: Int -> Int
-square x  =  x * x
-
-add :: Int -> Int -> Int
-add x y  =  x + y
-
-factorial :: Int -> Int
-cannot conjure
-
-factorial :: Int -> Int
-factorial x  =  foldr (*) 1 (enumFromTo 1 x)
-
-second :: [Int] -> Int
-second xs  =  head (tail xs)
-
-(++) :: [Int] -> [Int] -> [Int]
-xs ++ ys  =  foldr (:) ys xs
-
-reverse :: [Int] -> [Int]
-cannot conjure
-
-reverse :: [Int] -> [Int]
-reverse xs  =  foldr (foldr (:) . unit) [] xs
-
diff --git a/test/utils.hs b/test/utils.hs
--- a/test/utils.hs
+++ b/test/utils.hs
@@ -51,6 +51,11 @@
   , not $ isDec m (==0) (\x -> x-2 :: Int)
   ,       isDec m (==0) (\x -> x `div` 2 :: Int)
   ,       isDec m (==0) (\x -> x `quot` 2 :: Int)
+
+  , sets []  ==  [[] :: [Int]]
+  , sets [1]  ==  [[1], [] :: [Int]]
+  , sets [1,2]  ==  [[1,2], [1], [2], [] :: [Int]]
+  , sets [1,2,3]  ==  [[1,2,3],[1,2],[1,3],[1],[2,3],[2],[3],[] :: [Int]]
   ]
   where
   m  =  n `div` 60