diff --git a/HasCacBDD.cabal b/HasCacBDD.cabal
--- a/HasCacBDD.cabal
+++ b/HasCacBDD.cabal
@@ -1,5 +1,5 @@
 name:                HasCacBDD
-version:             0.1.0.0
+version:             0.1.0.1
 synopsis:            Haskell bindings for CacBDD
 homepage:            https://github.com/m4lvin/HasCacBDD
 license:             GPL-2
@@ -8,7 +8,7 @@
 maintainer:          malvin@w4eg.de
 category:            Data
 build-type:          Custom
-cabal-version:       >=1.23
+cabal-version:       1.24
 
 description: Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management.
              Original C++ code from <http://kailesu.net/CacBDD> and a C wrapper are included.
@@ -46,30 +46,13 @@
   cc-options:          -fPIC -shared
   ghc-options:         -pgml g++ -Wall -fPIC -fno-full-laziness
 
-test-suite example
-  default-language:    Haskell2010
-  type:                exitcode-stdio-1.0
-  main-is:             Example.hs
-  hs-source-dirs:      tests
-  build-depends:       base >=4.8,
-                       HasCacBDD
-  ghc-options:         -pgml g++ -Wall -fPIC -fno-full-laziness
-
-test-suite basics
-  default-language:    Haskell2010
-  type:                exitcode-stdio-1.0
-  main-is:             Basics.hs
-  hs-source-dirs:      tests
-  build-depends:       base >=4.8,
-                       HasCacBDD
-  ghc-options:         -Wall
-
-test-suite tautologies
+test-suite tests
   default-language:    Haskell2010
   type:                exitcode-stdio-1.0
-  main-is:             Tautologies.hs
+  main-is:             Main.hs
   hs-source-dirs:      tests
   build-depends:       base >=4.8,
                        HasCacBDD,
+                       hspec,
                        QuickCheck > 2.4
-  ghc-options:         -Wall -fhpc -fforce-recomp
+  ghc-options:         -Wall -threaded
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,8 +1,39 @@
 HasCacBDD
 =========
 
+[![Release](https://img.shields.io/github/release/m4lvin/HasCacBDD.svg)](https://github.com/m4lvin/HasCacBDD/releases)
+[![Hackage](https://img.shields.io/hackage/v/HasCacBDD.svg)](https://hackage.haskell.org/package/HasCacBDD)
 [![Build Status](https://travis-ci.org/m4lvin/HasCacBDD.svg?branch=master)](https://travis-ci.org/m4lvin/HasCacBDD)
 
 Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management.
 
 Original C++ code from <http://kailesu.net/CacBDD> and a C wrapper are included.
+
+
+# Getting Started
+
+1. Install C compilers and stack if necessary:
+
+       apt install build-essential git
+       curl -sSL https://get.haskellstack.org/ | sh
+
+2. Download, build and load the lastest version:
+
+       git clone https://github.com/m4lvin/HasCacBDD.git
+       cd HasCacBDD
+       stack setup
+       stack build
+       stack exec ghci
+
+    Note: `stack ghci` apparently does not work with the shared library.
+    You really need `stack build` and then `stack exec ghci`.
+
+3. Play :-)
+
+       λ> import Data.HasCacBDD
+       λ> var 5
+       Var 5 Top Bot
+       λ> neg (var 5)
+       Var 5 Bot Top
+       λ> dis (neg (var 3)) (var 3)
+       Top
diff --git a/hs/Data/HasCacBDD.hs b/hs/Data/HasCacBDD.hs
--- a/hs/Data/HasCacBDD.hs
+++ b/hs/Data/HasCacBDD.hs
@@ -10,7 +10,8 @@
   neg, con, dis, imp, equ, xor, conSet, disSet, xorSet,
   exists, forall, forallSet, existsSet,
   restrict, restrictSet, restrictLaw,
-  ifthenelse, gfp, relabel,
+  ifthenelse, gfp, relabel, relabelFun,
+  substit, substitSimul,
   -- * Evaluation
   evaluate, evaluateFun,
   -- * Get satisfying assignments
@@ -31,7 +32,7 @@
 import System.IO.Unsafe
 import Data.List (nub,(\\),sort)
 import Data.Maybe (fromJust)
-import Test.QuickCheck (Arbitrary, Gen, arbitrary, choose, oneof, sized, listOf)
+import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf)
 
 -- | The CacBDD datatype has no structure because
 -- from our perspective BDDs are just pointers.
@@ -41,7 +42,6 @@
 -- | An assignment of boolean values to variables/integers.
 type Assignment = [(Int,Bool)]
 
--- | We attach the free() finalizer to our BDDs.
 finalize :: Ptr CacBDD -> Bdd
 finalize ptr = Bdd (unsafePerformIO $ newForeignPtr finalizerFree ptr)
 
@@ -82,7 +82,6 @@
 manager = finalizeMgr (unsafePerformIO $ xBddManager_new (fromIntegral maximumvar))
 {-# NOINLINE manager #-}
 
--- | This should cover BDDOne, BddZero
 fromManager :: NullOp -> Bdd
 fromManager nulloperator = let (XBddManager mptr) = manager in
   finalize $ unsafePerformIO $
@@ -121,7 +120,7 @@
 restrictSet b bits = withTwoBDDs bdd_Restrict b (conSet $ map (\(n,bit) -> if bit then var n else neg (var n)) bits)
 {-# NOINLINE restrictSet #-}
 
--- | Restrict with a law
+-- | Restrict with a law. Note that the law is the second parameter!
 restrictLaw :: Bdd -> Bdd -> Bdd
 restrictLaw = withTwoBDDs bdd_Restrict
 {-# NOINLINE restrictLaw #-}
@@ -365,7 +364,7 @@
 allSatsWith allvars b = concatMap (completeAss allvars) (allSats b)
 
 -- | Given a set of all variables, get the number of satisfying assignments.
--- Note that allvars should be nub'd and sorted.
+-- Note that allvars must be nub'd and sorted.
 satCountWith :: [Int] -> Bdd -> Int
 satCountWith allvars b
   | b == top = 2 ^ length allvars
@@ -384,6 +383,7 @@
   Just partass -> Just $ head $ completeAss allvars partass
 
 -- | Relabel variables according to the given mapping.
+-- Note that the mapping list must be sorted!
 relabel :: [(Int,Int)] -> Bdd -> Bdd
 relabel [] b = b
 relabel rel@((n,newn):rest) b
@@ -394,6 +394,33 @@
                   EQ -> ifthenelse (var newn) (relabel rest (thenOf b)) (relabel rest (elseOf b))
                   GT -> ifthenelse (var (fromJust (firstVarOf b))) (relabel rel (thenOf b)) (relabel rel (elseOf b))
 
+-- | Relabel variables according to the given function.
+relabelFun :: (Int -> Int) -> Bdd -> Bdd
+relabelFun f b = case firstVarOf b of
+  Nothing -> b
+  Just m  -> ifthenelse (var (f m)) (relabelFun f (thenOf b)) (relabelFun f (elseOf b))
+
+-- | Substitute a BDD for a given variable in another BDD.
+substit :: Int -> Bdd -> Bdd -> Bdd
+substit n psi b =
+  case firstVarOf b of
+    Nothing -> b
+    Just k  -> case compare n k of
+      LT -> b
+      EQ -> ifthenelse psi (thenOf b) (elseOf b)
+      GT -> ifthenelse (var k) (substit n psi (thenOf b)) (substit n psi (elseOf b))
+
+-- | Simultaneous substitution of BDDs for variables.
+-- Note that this is not the same as folding `substit`.
+substitSimul :: [(Int,Bdd)] -> Bdd -> Bdd
+substitSimul []    b = b
+substitSimul repls b =
+  case firstVarOf b of
+    Nothing -> b
+    Just k  -> case lookup k repls of
+      Nothing  -> ifthenelse (var k) (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b)
+      Just psi -> ifthenelse psi     (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b)
+
 -- | Show internal statistics.
 showInfo :: IO ()
 showInfo = withForeignPtr mptr xBddManager_showInfo where (XBddManager mptr) = manager
@@ -401,6 +428,9 @@
 -- | QuickCheck Arbitrary instances for BDDs
 instance Arbitrary Bdd where
   arbitrary = sized randombdd
+  shrink b | b == top  = []
+           | b == bot  = []
+           | otherwise = [thenOf b, elseOf b]
 
 randomvarnumber :: Gen Int
 randomvarnumber = choose (0, 100)
@@ -425,4 +455,4 @@
   , forallSet <$> listOf randomvarnumber <*> smallerbdd
   ]
   where
-    smallerbdd = randombdd (min (n `div` 2) 10)
+    smallerbdd = randombdd (n `div` 2)
diff --git a/hs/Data/HasCacBDD/Visuals.hs b/hs/Data/HasCacBDD/Visuals.hs
--- a/hs/Data/HasCacBDD/Visuals.hs
+++ b/hs/Data/HasCacBDD/Visuals.hs
@@ -23,23 +23,20 @@
   | otherwise = "strict digraph g {\n" ++ links ++ sinks ++ rankings ++ "}" where
       (links,topdone) = genGraphStep [] myb
       genGraphStep :: [(Bdd,Int)] -> Bdd -> (String,[(Bdd,Int)])
-      genGraphStep done curB = case (lookup curB done, curB == top || curB == bot) of
-        (_     ,True) -> ("",done)
-        (Just _, _) -> ("",done)
-        (Nothing,False) ->
+      genGraphStep done curB =
+        if curB `elem` [top,bot] ++ map fst done then ("",done) else
             let
               thisn = if null done then 0 else maximum (map snd done) + 1
               thisnstr = show thisn
               (Just thisvar) = firstVarOf curB
               out1  = "n" ++ thisnstr ++ " [label=\"" ++ myShow thisvar ++ "\",shape=\"circle\"];\n"
-              lhs   = thenOf curB
+              (lhs, rhs) = (thenOf curB, elseOf curB)
               (lhsoutput,lhsdone) = genGraphStep ((curB,thisn):done) lhs
               (Just leftn) = lookup lhs lhsdone
               out2
                 | lhs == top = "n"++ thisnstr ++" -> Top;\n"
                 | lhs == bot = "n"++ thisnstr ++" -> Bot;\n"
                 | otherwise  = "n"++ thisnstr ++" -> n" ++ show leftn ++";\n" ++ lhsoutput
-              rhs   = elseOf curB
               (rhsoutput,rhsdone) = genGraphStep lhsdone rhs
               (Just rightn) = lookup rhs rhsdone
               out3
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,3 +1,3 @@
-resolver: lts-8.0
+resolver: lts-12.9
 packages:
 - '.'
diff --git a/tests/Basics.hs b/tests/Basics.hs
deleted file mode 100644
--- a/tests/Basics.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-module Main where
-
-import Data.HasCacBDD
-import System.Exit
-
-main :: IO ()
-main = do
-  putStrLn "\nRunning basic tests ..."
-  if all snd tests
-    then do
-      putStrLn "All passed."
-      exitSuccess
-    else do
-      putStrLn "FAILURES:"
-      let failures = filter (not.snd) tests
-      mapM_ (putStrLn . fst) failures
-      putStrLn "All results:"
-      mapM_ print tests
-      exitFailure
-
-tests :: [(String,Bool)]
-tests =
-  [ ("top == top", top == top)
-  , ("top /= bot", top /= bot)
-  , ("bot /= top", bot /= top)
-  , ("bot == bot", bot == bot)
-  , ("neg bot == top", neg bot == top)
-  , ("neg bot /= bot", neg bot /= bot)
-  , ("var 1 == var 1", var 1 == var 1)
-  , ("var 5 /= var 7", var 5 /= var 7)
-  , ("null (allSats bot)", null (allSats bot))
-  , ("allSats top == [[]]", allSats top == [[]])
-  , ("var 3 == con (var 3) top", var 3 == con (var 3) top)
-  , ("var 4 /= con (var 3) top", var 4 /= con (var 3) top)
-  , ("equ (var 1) (var 1) == top", equ (var 1) (var 1) == top)
-  , ("exists 1 (neg $ var 1) == top", exists 1 (neg $ var 1) == top)
-  , ("exists 1 (neg $ var 2) /= top", exists 1 (neg $ var 2) /= top)
-  , ("gfp (\b -> con b (var 3)) == var 3", gfp (\b -> con b (var 3)) == var 3)
-  , ("imp (conSet [var 1, var 0]) (var 1) == top", imp (conSet [var 1, var 0]) (var 1) == top)
-  , ("imp (conSet [var 0, var 1]) (var 0) == top", imp (conSet [var 0, var 1]) (var 0) == top)
-  , ("imp (con (var 0) (var 1)) (var 0) == top", imp (con (var 0) (var 1)) (var 0) == top)
-  , ("show top == \"Top\"", show top == "Top")
-  , ("show bot == \"Bot\"", show bot == "Bot")
-  ]
diff --git a/tests/Example.hs b/tests/Example.hs
deleted file mode 100644
--- a/tests/Example.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-module Main
-where
-
-import Data.HasCacBDD
-import System.Exit
-import System.IO
-
-main :: IO ()
-main = do
-  hSetBuffering stdout NoBuffering
-  putStrLn "Creating some BDDs:"
-  putStrLn $ "top : " ++ show top
-  putStrLn $ "bot : " ++ show bot
-  putStrLn $ "var1: " ++ show (var 1)
-  putStrLn $ "var1: " ++ show (var 1)
-  putStrLn $ "var2: " ++ show (var 2)
-  putStrLn "\nChecking some tautologies:"
-  print $ bot == bot
-  print $ top == top
-  print $ var 1 == var 1
-  print $ imp (var 1) (var 1) == top
-  print $ equ (var 1) (var 1) == top
-  print $ exists 1 (neg $ var 1) == top
-  print $ gfp (\b -> con b (var 3)) == var 3
-  print $ imp (conSet [var 1, var 0]) (var 1) == top
-  print $ imp (conSet [var 0, var 1]) (var 0) == top
-  print $ imp (con (var 0) (var 1)) (var 0) == top
-  putStrLn "\nAnd some contradictions:"
-  print $ bot == top
-  print $ top == bot
-  print $ var 1 == top
-  print $ dis (var 1) (neg $ var 2) == top
-  print $ dis (var 1) (var 2) == top
-  print $ var 1 == var 2
-  print $ forall 1 (var 1) == top
-  putStrLn "\nLaws from de Morgan:"
-  print $ dis (neg $ var 1) (neg $ var 2) == neg (con (var 1) (var 2))
-  print $ con (neg $ var 1) (neg $ var 2) == neg (dis (var 1) (var 2))
-  putStrLn "\nThe example from CacBDDs main.cpp: (!x[4] + !x[6]) * (!x[3] + !x[6]) * (!x[2] + !x[5])"
-  let cacExample = conSet [ dis (neg (var 4)) (neg (var 6)) , neg (var 3) `dis` neg (var 6), neg (var 2) `dis` neg (var 5) ]
-  print cacExample
-  print $ cacExample == top
-  putStrLn "Good Bye."
-  exitSuccess
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,124 @@
+module Main where
+
+import Data.HasCacBDD
+import Data.List (nub)
+import Data.Maybe (fromJust,isNothing)
+import Data.Tuple (swap)
+import Test.QuickCheck
+import Test.Hspec
+import Test.Hspec.QuickCheck
+
+main :: IO ()
+main  = hspec $ do
+  describe "Examples" $ do
+    describe "Creating BDDs" $ do
+      it "top == Top" $ show top `shouldBe` "Top"
+      it "" $ show bot `shouldBe` "Bot"
+      it "" $ show (var 1) `shouldBe` "Var 1 Top Bot"
+      it "" $ show (var 1) `shouldBe` "Var 1 Top Bot"
+      it "" $ show (var 2) `shouldBe` "Var 2 Top Bot"
+    describe "Some tautologies" $ do
+      it "bot == bot" $ bot `shouldBe` bot
+      it "top == top" $ top `shouldBe` top
+      it "var 1 == var 1" $ var 1 `shouldBe` var 1
+      it "imp (var 1) (var 1) == top" $ imp (var 1) (var 1) `shouldBe` top
+      it "equ (var 1) (var 1) == top" $ equ (var 1) (var 1) `shouldBe` top
+      it "exists 1 (neg $ var 1) == top" $ exists 1 (neg $ var 1) `shouldBe` top
+      it "gfp (\b -> con b (var 3)) == var 3" $ gfp (\b -> con b (var 3)) `shouldBe` var 3
+      it "imp (conSet [var 1, var 0]) (var 1) == top" $ imp (conSet [var 1, var 0]) (var 1) `shouldBe` top
+      it "imp (conSet [var 0, var 1]) (var 0) == top" $ imp (conSet [var 0, var 1]) (var 0) `shouldBe` top
+      it "imp (con (var 0) (var 1)) (var 0) == top" $ imp (con (var 0) (var 1)) (var 0) `shouldBe` top
+    describe "Some non-tautologies" $ do
+      it "bot /= top" $ bot `shouldNotBe` top
+      it "top /= bot" $ top `shouldNotBe` bot
+      it "var 1 /= top" $ var 1 `shouldNotBe` top
+      it "dis (var 1) (neg $ var 2) /= top" $ dis (var 1) (neg $ var 2) `shouldNotBe` top
+      it "dis (var 1) (var 2) /= top" $ dis (var 1) (var 2) `shouldNotBe` top
+      it "var 1 /= var 2" $ var 1 `shouldNotBe` var 2
+      it "forall 1 (var 1) /= top" $ forall 1 (var 1) `shouldNotBe` top
+    describe "Laws from de Morgan:" $ do
+      it "" $ dis (neg $ var 1) (neg $ var 2) == neg (con (var 1) (var 2))
+      it "" $ con (neg $ var 1) (neg $ var 2) == neg (dis (var 1) (var 2))
+    it "The example from CacBDDs main.cpp (~x[4] + ~x[6]) * (~x[3] + ~x[6]) * (~x[2] + ~x[5]) /= top" $
+      conSet [ dis (neg (var 4)) (neg (var 6)) , neg (var 3) `dis` neg (var 6), neg (var 2) `dis` neg (var 5) ] `shouldNotBe` top
+    it "showInfo works" $
+      showInfo `shouldReturn` ()
+  describe "Basics" $ do
+    it "top == top" $ top `shouldBe` top
+    it "top /= bot" $ top `shouldNotBe` bot
+    it "bo /= top" $ bot `shouldNotBe` top
+    it "bot == bot" $ bot `shouldBe` bot
+    it "neg bot == top" $ neg bot `shouldBe` top
+    it "neg bot /= bot" $ neg bot `shouldNotBe` bot
+    it "var 1 == var 1" $ var 1 `shouldBe` var 1
+    it "var 5 == var 7" $ var 5 `shouldNotBe` var 7
+    it "null (allSats bot)" $ null (allSats bot)
+    it "allSats top `==` [[]]" $ allSats top `shouldBe` [[]]
+    it "var 3 == con (var 3) top" $ var 3 `shouldBe` con (var 3) top
+    it "var 4 /= con (var 3) top" $ var 4 `shouldNotBe` con (var 3) top
+    it "equ (var 1) (var 1) == top" $ equ (var 1) (var 1) `shouldBe` top
+    it "exists 1 (neg $ var 1) == top" $ exists 1 (neg $ var 1) `shouldBe` top
+    it "exists 1 (neg $ var 2) /= top" $ exists 1 (neg $ var 2) `shouldNotBe` top
+    it "gfp (\b -> con b (var 3)) == var 3" $ gfp (\b -> con b (var 3)) `shouldBe` var 3
+    it "imp (conSet [var 1,var 0]) (var 1) == top" $ imp (conSet [var 1,var 0]) (var 1) `shouldBe` top
+    it "imp (conSet [var 0,var 1]) (var 0) == top" $ imp (conSet [var 0,var 1]) (var 0) `shouldBe` top
+    it "imp (con (var 0) (var 1)) (var 0) == top" $ imp (con (var 0) (var 1)) (var 0) `shouldBe` top
+    it "show top == \"Top\"" $ show top `shouldBe` "Top"
+    it "show bot == \"Bot\"" $ show bot `shouldBe` "Bot"
+  describe "QuickCheck Properties" $ do
+    prop "selfEqual"      (\b -> (b::Bdd) == b)
+    prop "idSymmetry"     (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a))
+    prop "singleNegation" (\b -> neg b /= b)
+    prop "doubleNegation" (\b -> neg (neg b) == b)
+    prop "selfImp"        (\b -> imp b b == top)
+    prop "selfEqu"        (\b -> equ b b == top)
+    prop "selfXor"        (\b -> xor b b == bot)
+    prop "excludedMiddle" (\b -> b `dis` neg b == top)
+    prop "deMorganOne"    (\a b -> neg (a `con` b) == (neg a `dis` neg b))
+    prop "deMorganTwo"    (\a b -> neg (a `dis` b) == (neg a `con` neg b))
+    prop "identityOne"    (\as b -> conSet as `imp` b  ==  disSet (map neg as) `dis` b)
+    prop "conElim"        (\a b -> imp (con a b) a == top)
+    prop "conElim3"       (\a b c -> imp (conSet [a, b, c]) a == top)
+    prop "negNotEqual"    (\b -> neg b /= b)
+    prop "quantifDuality" (forAll (elements [0..maximumvar]) (\n b -> forall n b == neg (exists n (neg b))))
+    prop "allSats"        (\b -> all (\s -> restrictSet b s == top) (allSats b))
+    prop "anySat"         (\b -> if b==bot then isNothing (anySat b) else restrictSet b (fromJust $ anySat b) == top)
+    prop "ifthenelse"     (\a b c -> ifthenelse a b c == neg (dis (con a (neg b)) (con (neg a) (neg c))))
+    prop "ravel-unravel"  (\b -> b == ravel (unravel b))
+    prop "firstVarOf"     (\b -> if b `elem` [bot,top] then isNothing (firstVarOf b) else Just (head (allVarsOfSorted b)) == firstVarOf b)
+    prop "maxVarOf"       (\b -> if b `elem` [bot,top] then isNothing (maxVarOf b) else Just (last (allVarsOfSorted b)) == maxVarOf   b)
+    prop "thenOf"         (\b -> if b `elem` [bot,top] then thenOf b == b else thenOf b == restrict b (fromJust $ firstVarOf b, True ))
+    prop "elseOf"         (\b -> if b `elem` [bot,top] then elseOf b == b else elseOf b == restrict b (fromJust $ firstVarOf b, False))
+    prop "deMorganOneSet" (\as -> neg (conSet as) ==  disSet (map neg as))
+    prop "deMorganTwoSet" (\as -> neg (disSet as) ==  conSet (map neg as))
+    prop "conSetCommute"  (\a as -> conSet (a:as) == con (conSet as) a)
+    prop "disSetCommute"  (\a as -> disSet (a:as) == dis (disSet as) a)
+    prop "xorSetNeg3"     (\a b c -> xorSet [a,b,c] == xorSet [neg a, b, neg c])
+    prop "xorSetCommute3" (\a b c -> xorSet [a,b,c] == xor (xorSet [a,b]) c)
+    prop "xorSetCommute4" (\a b c d -> xorSet [a,b,c,d] == xor (xorSet [b,c,a]) d)
+    prop "gfpCon"         (\b -> gfp (`con` b) == b)
+    prop "sizeNeg"        (\b -> sizeOf b == sizeOf (neg b))
+    prop "restrictLaw"    (\a b -> b `imp` equ (restrictLaw a b) a == top)
+    prop "evaluate"       (\b -> all (\s -> evaluate b s == Just True) (allSatsWith (allVarsOf b) b))
+    prop "evaluateFun"    (\b -> all (\s -> evaluateFun b (\n -> fromJust $ lookup n s)) (allSats b))
+    prop "allSatsWith"    (\b -> all (\s -> restrictSet b s == top) (allSatsWith (allVarsOf b) b))
+    prop "anySatWith"     (\b -> let vs = allVarsOf b in if b==bot then isNothing (anySatWith vs b) else restrictSet b (fromJust $ anySatWith vs b) == top)
+    prop "satCountWith"   (\b -> let vs = allVarsOf b in length (allSatsWith vs b) == satCountWith vs b)
+    prop "subsOf"         (\b -> all (`elem` subsOf b) (subsOf $ thenOf b))
+    prop "relabel"        (\b c -> let
+                                      vs = reverse $ nub (allVarsOf b ++ allVarsOf c)
+                                      mapping = zip vs (map (+100) vs)
+                                      gnippam = map swap mapping
+                                   in
+                                      relabel gnippam (relabel mapping b) == b)
+    prop "relabelFun"    (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) == a)
+    prop "substit"       (\b c -> substit 1 b c == ifthenelse b (restrict c (1,True)) (restrict c (1,False)))
+    prop "show"          (\a b -> (show (unravel a) == show (unravel b)) == (a == (b::Bdd)))
+    prop "showList"      (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd)))
+  describe "QuickCheck Expected Failures" $ do
+    prop "wrong deMorganOne" $
+      expectFailure (\a b -> neg (a `con` b) === (neg a `con` neg b))
+    prop "wrong deMorganTwo" $
+      expectFailure (\a b -> neg (a `dis` b) === (neg a `dis` neg b))
+    modifyMaxSuccess (* 1000) $ prop "folding substit is not the same as substitSimul" $
+      expectFailure (\b1 b2 c -> foldl (flip $ uncurry substit) c [(1,b1),(2,b2)] === substitSimul [(1,b1),(2,b2)] c)
diff --git a/tests/Tautologies.hs b/tests/Tautologies.hs
deleted file mode 100644
--- a/tests/Tautologies.hs
+++ /dev/null
@@ -1,63 +0,0 @@
-module Main where
-
-import Control.Monad
-import Data.HasCacBDD
-import Data.List
-import Data.Maybe
-import Data.Tuple
-import Text.Printf
-import Test.QuickCheck
-import Test.QuickCheck.Test
-import System.Exit
-
-main :: IO ()
-main  = do
-  results <- mapM (\(s,a) -> printf "%-25s: " s >> a) tests
-  unless (all isSuccess results) exitFailure
-  showInfo
-
-tests :: [(String, IO Result)]
-tests  =
-  [("selfEqual",      quickCheckResult (\b -> (b::Bdd) == b))
-  ,("idSymmetry",     quickCheckResult (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a)))
-  ,("singleNegation", quickCheckResult (\b -> neg b /= b))
-  ,("doubleNegation", quickCheckResult (\b -> neg (neg b) == b))
-  ,("selfImp",        quickCheckResult (\b -> imp b b == top))
-  ,("selfEqu",        quickCheckResult (\b -> equ b b == top))
-  ,("selfXor",        quickCheckResult (\b -> xor b b == bot))
-  ,("excludedMiddle", quickCheckResult (\b -> b `dis` neg b == top))
-  ,("deMorganOne",    quickCheckResult (\a b -> neg (a `con` b) == (neg a `dis` neg b)))
-  ,("deMorganTwo",    quickCheckResult (\a b -> neg (a `dis` b) == (neg a `con` neg b)))
-  ,("identityOne",    quickCheckResult (\as b -> conSet as `imp` b  ==  disSet (map neg as) `dis` b))
-  ,("conElim",        quickCheckResult (\a b -> imp (con a b) a == top))
-  ,("conElim3",       quickCheckResult (\a b c -> imp (conSet [a, b, c]) a == top))
-  ,("negNotEqual",    quickCheckResult (\b -> neg b /= b))
-  ,("quantifDuality", quickCheckResult (forAll (elements [0..maximumvar]) (\n b -> forall n b == neg (exists n (neg b)))))
-  ,("allSats",        quickCheckResult (\b -> all (\s -> restrictSet b s == top) (allSats b)))
-  ,("anySat",         quickCheckResult (\b -> if b==bot then isNothing (anySat b) else restrictSet b (fromJust $ anySat b) == top))
-  ,("ifthenelse",     quickCheckResult (\a b c -> ifthenelse a b c == neg (dis (con a (neg b)) (con (neg a) (neg c)))))
-  ,("ravel-unravel",  quickCheckResult (\b -> b == ravel (unravel b)))
-  ,("firstVarOf",     quickCheckResult (\b -> if b `elem` [bot,top] then isNothing (firstVarOf b) else Just (head (allVarsOfSorted b)) == firstVarOf b))
-  ,("maxVarOf",       quickCheckResult (\b -> if b `elem` [bot,top] then isNothing (maxVarOf b) else Just (last (allVarsOfSorted b)) == maxVarOf   b))
-  ,("thenOf",         quickCheckResult (\b -> if b `elem` [bot,top] then thenOf b == b else thenOf b == restrict b (fromJust $ firstVarOf b, True )))
-  ,("elseOf",         quickCheckResult (\b -> if b `elem` [bot,top] then elseOf b == b else elseOf b == restrict b (fromJust $ firstVarOf b, False)))
-  ,("deMorganOneSet", quickCheckResult (\as -> neg (conSet as) ==  disSet (map neg as)))
-  ,("deMorganTwoSet", quickCheckResult (\as -> neg (disSet as) ==  conSet (map neg as)))
-  ,("xorSetCommute",  quickCheckResult (\a as -> xorSet (a:as) == xor (xorSet as) a))
-  ,("gfpCon",         quickCheckResult (\b -> gfp (`con` b) == b))
-  ,("sizeNeg",        quickCheckResult (\b -> sizeOf b == sizeOf (neg b)))
-  ,("restrictLaw",    quickCheckResult (\a b -> b `imp` equ (restrictLaw a b) a == top))
-  ,("evaluate",       quickCheckResult (\b -> all (\s -> evaluate b s == Just True) (allSatsWith (allVarsOf b) b)))
-  ,("evaluateFun",    quickCheckResult (\b -> all (\s -> evaluateFun b (\n -> fromJust $ lookup n s)) (allSats b)))
-  ,("allSatsWith",    quickCheckResult (\b -> all (\s -> restrictSet b s == top) (allSatsWith (allVarsOf b) b)))
-  ,("anySatWith",     quickCheckResult (\b -> let vs = allVarsOf b in if b==bot then isNothing (anySatWith vs b) else restrictSet b (fromJust $ anySatWith vs b) == top))
-  ,("satCountWith",   quickCheckResult (\b -> let vs = allVarsOf b in length (allSatsWith vs b) == satCountWith vs b))
-  ,("subsOf",         quickCheckResult (\b -> all (`elem` subsOf b) (subsOf $ thenOf b)))
-  , let relabelTest b c = relabel gnippam (relabel mapping b) == b where
-          vs = reverse $ nub (allVarsOf b ++ allVarsOf c)
-          mapping = zip vs (map (+100) vs)
-          gnippam = map swap mapping
-    in ("relabel",    quickCheckResult relabelTest)
-  , ("show",          quickCheckResult (\a b -> (show (unravel a) == show (unravel b)) == (a == (b::Bdd))))
-  , ("showList",      quickCheckResult (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd))))
-  ]