diff --git a/examples/Cubism.hs b/examples/Cubism.hs
new file mode 100644
--- /dev/null
+++ b/examples/Cubism.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE TupleSections #-}
+{-# language LambdaCase #-}
+
+import Prelude hiding ((&&),(||),not,and,or)
+import OBDD
+import OBDD.Cube
+import System.Environment (getArgs)
+
+data T = In | L | R | Out   deriving (Eq, Ord, Show)
+
+vars n = (,) <$> [1..n] <*> [L,R,Out]
+
+main = getArgs >>= \ case
+ []  -> out $ cnf $ form add 3
+ [ "add", s] -> out $ cnf $ form add $ read s
+ [ "mul", s] -> out $ cnf $ form mul $ read s
+ [ "hist", s] -> out $ cnf $ function (read s) hist
+ [ "sort", s] -> out $ cnf $ function (read s) sort
+ "king" : cs -> out $ cnf $ constrained_function 9 $ king (map read cs)
+
+out cs = mapM_ (\(k,v) -> putStrLn $ show k ++ " " ++ nice v)
+       $ zip [0..] cs
+
+function w f = 
+  let input = map ( variable . (, In) ) [1 .. w]
+      output = map ( variable . (, Out) ) [1 .. ]
+  in  and $ zipWith equiv (f input) output
+
+constrained_function w f =
+  let input = map ( variable . (, In) ) [1 .. w]
+      output = map ( variable . (, Out) ) [1 .. ]
+      (c,out) = f input
+  in  and $ c : zipWith equiv out output
+
+-- | for MM 12/16
+king hs (this : neighbours) =
+  let ys = hist neighbours
+      cs = map (\ h -> this && ys !! h) hs
+  in  ( this ==> or cs , cs )
+
+sort xs =
+  let insert ys x =
+        zipWith ( \ a b -> a || b && x ) ys ( true : ys )
+  in  foldl insert (replicate (length xs) false) xs
+
+-- | histogram xs == ys where  ys !! i <=> exactly i xs,
+-- produces a one-hot bit vector.
+-- length output = 1 + length input
+hist xs =
+  let insert ys x =
+        zipWith ( \ a b -> choose a b x ) ys ( false : ys )
+  in  foldl insert (true : replicate (length xs) false) xs
+  
+form fun n =
+  let make f = ( \ v -> variable (v,f)) <$> [1..n]
+      (pre,post) = splitAt n $ fun (make L) (make R)
+  in  not (or post) && and ( zipWith equiv pre $ make Out )
+
+mul [] ys = []
+mul (x:xs) ys = add (map (&& x) ys) $ false : mul xs ys
+
+add xs ys =
+  let go c [] [] = [c]
+      go c (x:xs) [] = let (r,d) = halfadd c x in r : go d xs []
+      go c [] (y:ys) = let (r,d) = halfadd c y in r : go d ys []
+      go c (x:xs) (y:ys) = let (r,d) = fulladd c x y in r : go d xs ys
+  in  go false xs ys
+      
+halfadd x y = (xor x y , x && y)
+
+fulladd x y z =
+  let (r , c)  = halfadd x y
+      (s , d) = halfadd r z
+  in  (s, c || d)
+
diff --git a/examples/MM0916.hs b/examples/MM0916.hs
--- a/examples/MM0916.hs
+++ b/examples/MM0916.hs
@@ -64,9 +64,8 @@
     $ (  exactly q $ queen <$> positions n )
     : ( for ( positions n) $ \ p -> 
       (not $ queen p) || (not $ attacked p) )
-    ++ ( for (positions n) $ \ p -> 
-     implies (attacked p) $ exactly a $ for directions $ \ d ->
-       r A.! (d,p) )
+    ++ ( for (positions n) $ \ p ->  attacked p ==>
+           ( exactly a $ for directions $ \ d -> r A.! (d,p)))
     
 
 -- | ray n ! (d,p) == looking in direction d from p,
@@ -96,8 +95,8 @@
   else exactly_rectangle k xs
 
 exactly_rectangle n xs = last $ 
-  foldl ( \ cs x -> zipWith ( \ a b -> ite x a b )
-                    (false : cs) cs 
+  foldl ( \ cs x -> zipWith ( \ a b -> choose a b x )
+                    cs (false : cs) 
         ) (true : replicate n false) xs
 
 exactly_direct k xs = atmost k xs && atleast k xs
diff --git a/examples/Queens.hs b/examples/Queens.hs
--- a/examples/Queens.hs
+++ b/examples/Queens.hs
@@ -13,11 +13,11 @@
 
 import OBDD (OBDD)
 import qualified OBDD
-import qualified OBDD.Data (toDot)
 
 import Control.Monad ( guard )
 import System.Environment ( getArgs )
-import qualified Data.Set 
+import qualified Data.Set
+import qualified Data.Text.IO as T
 
 type Position = (Int,Int)
 
@@ -74,4 +74,4 @@
     m <- OBDD.some_model d
     print m
 
-    -- writeFile "Queens.dot" $ OBDD.Data.toDot d
+    -- T.writeFile "Queens.dot" $ OBDD.toDot d
diff --git a/examples/Queens2.hs b/examples/Queens2.hs
--- a/examples/Queens2.hs
+++ b/examples/Queens2.hs
@@ -38,12 +38,12 @@
 
 atmostone xs =
   let go (n,o) [] = n || o
-      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs
+      go (n,o) (x:xs) = go (choose n false x, choose o n x) xs
   in  go (true,false) xs
 
 exactlyone xs =
   let go (n,o) [] = o
-      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs
+      go (n,o) (x:xs) = go (choose n false x, choose o n x) xs
   in  go (true,false) xs
 
 handle check f n = OBDD.and $ do
diff --git a/examples/Sort.hs b/examples/Sort.hs
--- a/examples/Sort.hs
+++ b/examples/Sort.hs
@@ -29,7 +29,7 @@
 exactlyone :: [Bit] -> Bit
 exactlyone xs =
   let go (n,o) [] = o
-      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs
+      go (n,o) (x:xs) = go (choose n false x, choose o n x) xs
   in  go (true,false) xs
 
 -- | (weakly) increasing sequence of bits
@@ -43,7 +43,7 @@
 lt xs ys = or $ zipWith (\x y -> not x && y) xs ys
 
 leq :: Num -> Num -> Bit
-leq xs ys = and $ zipWith implies xs ys
+leq xs ys = and $ zipWith (==>) xs ys
 
 type Comp = (Int,Int)
 
@@ -86,7 +86,7 @@
       f = compat (args s) c && form s
   in  s { comps = cs'
         , poset = -- mkposet cs'
-	    transitive_closure $ S.insert c $ poset s
+            transitive_closure $ S.insert c $ poset s
         , form = f
         , size = number_of_models (vars w) f
         }
diff --git a/obdd.cabal b/obdd.cabal
--- a/obdd.cabal
+++ b/obdd.cabal
@@ -1,5 +1,5 @@
 Name:                obdd
-Version:             0.6.1
+Version:             0.8.1
 Cabal-Version:       >= 1.8
 Build-type: Simple
 Synopsis:            Ordered Reduced Binary Decision Diagrams
@@ -38,9 +38,9 @@
     Location: git://github.com/jwaldmann/haskell-obdd.git
 
 Library
-    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array, process
+    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array, process-extras, ersatz, text
     Hs-Source-Dirs:	     src
-    Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property, OBDD.Linopt
+    Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property, OBDD.Display, OBDD.Linopt, OBDD.Cube
     Other-Modules:	     OBDD.IntIntMap, OBDD.VarIntIntMap
     ghc-options: -funbox-strict-fields
 
@@ -50,12 +50,18 @@
     Main-Is: Placement.hs
     Build-Depends: base, containers, obdd
 
+test-suite obdd-cubism
+    Hs-Source-Dirs : examples
+    Type: exitcode-stdio-1.0
+    Main-Is: Cubism.hs
+    Build-Depends: base, containers, obdd
+
 test-suite obdd-queens
     Hs-Source-Dirs : examples
     Type: exitcode-stdio-1.0
     Main-Is: Queens.hs
     ghc-options: -threaded -rtsopts
-    Build-Depends: base, containers, obdd
+    Build-Depends: base, containers, obdd, text
 
 test-suite obdd-queens2
     Hs-Source-Dirs : examples
diff --git a/src/OBDD.hs b/src/OBDD.hs
--- a/src/OBDD.hs
+++ b/src/OBDD.hs
@@ -7,15 +7,24 @@
 
 module OBDD 
 
-( OBDD, display
+( module OBDD.Data
 , module OBDD.Property
 , module OBDD.Operation
+, module OBDD.Display
 , module OBDD.Make
 ) 
 
 where
 
-import OBDD.Data ( OBDD, display )
+import OBDD.Data ( OBDD , size
+                 , null, satisfiable
+                 , number_of_models
+                 , variables, paths, models
+                 , some_model
+                 , fold, foldM
+                 , full_fold, full_foldM
+                 )
 import OBDD.Property
 import OBDD.Operation
+import OBDD.Display
 import OBDD.Make
diff --git a/src/OBDD/Cube.hs b/src/OBDD/Cube.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD/Cube.hs
@@ -0,0 +1,94 @@
+{-# language FlexibleContexts #-}
+{-# LANGUAGE TupleSections #-}
+
+module OBDD.Cube where
+
+import Prelude hiding ((&&),(||),not,and,or)
+import qualified Prelude
+import OBDD
+
+import qualified Data.Bool 
+import Control.Monad (guard)
+import Control.Applicative
+
+import qualified Data.Map.Strict as M
+import qualified Data.Set as S
+import Data.List (partition, sortOn)
+
+import Debug.Trace
+
+type Cube v = M.Map v Bool
+
+primes :: Ord v => OBDD v -> [Cube v]
+primes d =
+  let process m = M.fromList $ do
+        ((v,Sign), b) <- M.toList m
+        return (v, b)
+  in map process $ paths $ prime d
+
+nice :: Show v => Cube v -> String
+nice c = "(" ++ do
+    (v,b) <- M.toList c
+    (if b then " " else " -") ++ show v
+  ++ ")"
+
+data Check = Sign | Occurs | Original
+           deriving (Eq, Ord, Show)
+
+sign v = variable (v, Sign)
+occurs v = variable (v, Occurs)
+original v = variable (v, Original)
+
+process c = M.fromList $ do
+        ((v,Occurs),True) <- M.toList c
+        return (v, c M.! (v,Sign))
+
+
+-- | O. Coudert , J. C. Madre:
+-- http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3330
+
+prime :: Ord v => OBDD v -> OBDD (v, Check)
+prime = snd
+  . fold ( \ b -> ( bool b, bool b ))
+         ( \ v (fl,pl) (fr,pr) -> ( choose fl fr (variable v)
+               , let common = prime (fl && fr)
+                 in      not (occurs v) && common
+                     || occurs v && not (sign v) && pl && not common
+                     || occurs v &&     (sign v) && pr && not common
+               )
+         )
+
+
+-- * naive way of finding a minimal set of clauses.
+
+dnf f =
+  let ps = primes f
+      ms = models (variables f) f
+      covering = do
+        m <- ms
+        return $ S.fromList $ do
+                   (i,p) <- zip [0..] ps
+                   guard $ M.isSubmapOf p m
+                   return i
+      cost = M.fromList $ zip [0..] $ map M.size ps
+      r = greed cost covering
+  in  map (ps !!) $ S.toList r
+
+
+cnf f = map (M.map Prelude.not) $ dnf $ not f
+
+greed cost [] = S.empty
+greed cost could =
+  let count = M.unionsWith (+) $ do
+        c <- could
+        return $ M.fromList $ zip (S.toList c) $ repeat 1
+      this = fst
+           $ head
+           $ sortOn snd
+           $ map (\(k,v) -> (k, (negate v, cost M.! k)))
+           $ M.toList count 
+  in    S.insert this
+      $ greed cost $ filter ( \p -> S.notMember this p ) could
+
+clause c = and $ do (v,b) <- M.toList c ; return $ unit v b
+
diff --git a/src/OBDD/Data.hs b/src/OBDD/Data.hs
--- a/src/OBDD/Data.hs
+++ b/src/OBDD/Data.hs
@@ -14,10 +14,10 @@
 -- * for external use
 , null, satisfiable
 , number_of_models
-, some_model, all_models
+, variables, paths, models
+, some_model
 , fold, foldM
 , full_fold, full_foldM
-, toDot, display
 -- * for internal use
 , Node (..)
 , make
@@ -55,7 +55,6 @@
 import Control.Monad ( forM, guard, void )
 import qualified Control.Monad ( foldM )
 import Data.Functor.Identity
-import System.Process
 import Data.List (isPrefixOf, isSuffixOf)
 
 import Prelude hiding ( null )
@@ -143,7 +142,7 @@
      -> ( v -> a -> a -> m a )
      -> OBDD v -> m a
 full_foldM vars leaf branch o = do
-    let vs = S.toAscList vars
+    let vs = S.toAscList $ S.union (variables o) vars
         low = head vs
         m = M.fromList $ zip vs $ tail vs
         up v = M.lookup v m
@@ -225,14 +224,25 @@
         Just m <- some_model t
         return $ Just $ M.insert v p m 
 
--- | list of all models (WARNING not using 
--- variables that had been deleted)
-all_models :: Ord v => OBDD v -> [ Map v Bool ]
-all_models = 
+-- | all variables that occur in the nodes
+variables :: Ord v => OBDD v -> S.Set v
+variables f = fold (\ b ->  S.empty )
+         ( \ v l r -> S.insert v $ S.union l r ) f
+
+-- | list of all paths
+paths :: Ord v => OBDD v -> [ Map v Bool ]
+paths = 
   fold ( bool [] [ M.empty ] )
        ( \ v l r -> (M.insert v False <$> l)
                  ++ (M.insert v True  <$> r) )
 
+-- | list of all models (a.k.a. minterms)
+models vars =
+  full_fold vars ( bool [] [ M.empty ] )
+       ( \ v l r -> (M.insert v False <$> l)
+                 ++ (M.insert v True  <$> r) )
+  
+
 select_one :: [a] -> IO a
 select_one xs | not ( Prelude.null xs ) = do
     i <- System.Random.randomRIO ( 0, length xs - 1 )
@@ -299,57 +309,3 @@
       check_var_ordering l ; check_var_ordering r
       register n
     _ -> register n
-
--- | Calls the @dot@ executable (must be in @$PATH@) to draw a diagram
--- in an X11 window. Will block until this window is closed.
--- Window can be closed gracefully by typing  'q'  when it has focus.
-display :: Show v => OBDD v -> IO ()
-display d = void $ readProcess "dot" [ "-Tx11" ] $ toDot d
-
--- | toDot outputs a string in format suitable for input to the "dot" program
--- from the graphviz suite.
-toDot :: (Show v) => OBDD v -> String
-toDot (OBDD idmap _ _ top _) =
-    unlines [ "digraph BDD {"
-            -- Start in oval mode
-            , "node[shape=oval];"
-            , evalState (helper $ idToNode top) S.empty
-            , "}"
-            ]
-  where
-    idToNode =
-        let getNode = \i -> case i of
-                          0 -> Leaf False
-                          1 -> Leaf True
-                          _ -> idmap IM.! i
-        in id &&& getNode
-
-    unquote s = if isPrefixOf "\"" s && isSuffixOf "\"" s
-                then init $ tail s
-                else s
-    mkLabel lbl = "[label=\"" ++ unquote lbl ++ "\"];"
-
-    helper (thisId, Leaf b) = return $
-        -- switch to rectangle nodes for the leaf, before going back to ovals.
-        unlines [ "node[shape=rectangle];"
-                , show thisId ++ mkLabel (show b)
-                , "node[shape=oval];"
-                ]
-    helper (thisId, Branch vid l r) = do
-        -- Ensure we don't traverse children multiple times, if we have more
-        -- than one edge into a given node.
-        beenHere <- gets (thisId `S.member`)
-        if beenHere
-            then return ""
-            else do
-                lstr <- helper $ idToNode l
-                rstr <- helper $ idToNode r
-                modify (thisId `S.insert`)
-                let idStr = show thisId
-                return $ unlines
-                   [ idStr ++ mkLabel (show vid)
-                   , lstr
-                   , idStr ++ "->" ++ show l ++ mkLabel "0"
-                   , rstr
-                   , idStr ++ "->" ++ show r ++ mkLabel "1"
-                   ]
diff --git a/src/OBDD/Display.hs b/src/OBDD/Display.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD/Display.hs
@@ -0,0 +1,70 @@
+{-# language OverloadedStrings #-}
+
+module OBDD.Display where
+
+import OBDD.Data (OBDD, foldM)
+import Control.Monad (void)
+import Control.Monad.RWS (RWS, evalRWS, tell, get, put)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Data.Monoid
+import System.Process.Text
+
+-- | Calls the @dot@ executable (must be in @$PATH@)
+-- to draw a diagram in an X11 window.
+-- Will block until this window is closed.
+-- Window can be closed gracefully
+-- by typing  'q'  when it has focus.
+display :: (Ord v, Show v) => OBDD v -> IO ()
+display d = void
+  $ readProcessWithExitCode "dot" [ "-Tx11" ]
+  $ toDot False d
+
+-- | same as @display@, but does not show the @False@ node
+-- and the edges pointing to @False@.
+display' :: (Ord v, Show v) => OBDD v -> IO ()
+display' d = void
+  $ readProcessWithExitCode "dot" [ "-Tx11" ]
+  $ toDot True d
+
+-- | a textual representation of the BDD that is suitable
+-- as input to the "dot" program from the graphviz suite.
+toDot :: (Ord v, Show v)
+  => Bool -- ^ suppress pointers to False
+  -> OBDD v -> Text
+toDot suppress_false =
+    snd
+  . ( \ m -> evalRWS (do tell "digraph BDD {"; m; tell "}" ) () 0 )
+  . foldM
+  ( \ b -> if not b && suppress_false then return Nothing else do
+     this <- fresh
+     tell $ T.unlines
+       [ "node[shape=rectangle];"
+       , text this <> mkLabel (text b)
+       , "node[shape=oval];"
+       ]
+     return $ Just this
+  )
+  ( \ v ml mr -> do
+     this <- fresh
+     tell $ text this <> mkLabel (text v)
+     case ml of
+       Just l -> tell $ text this <> "->" <> text l <> mkLabel "0"
+       Nothing -> return ()
+     case mr of
+       Just r -> tell $ text this <> "->" <> text r <> mkLabel "1"
+       Nothing -> return ()
+     return $ Just this
+  )
+
+fresh :: Monoid b => RWS a b Int Int
+fresh = do this <- get ; put $! succ this ; return this
+
+mkLabel lbl = "[label=\"" <> unquote lbl <> "\"];"
+
+unquote s =
+  if T.isPrefixOf "\"" s && T.isSuffixOf "\"" s
+  then T.init $ T.tail s
+  else s
+
+text x = T.pack $ show x
diff --git a/src/OBDD/Linopt.hs b/src/OBDD/Linopt.hs
--- a/src/OBDD/Linopt.hs
+++ b/src/OBDD/Linopt.hs
@@ -8,8 +8,8 @@
 -- | solve the constrained linear optimisation problem:
 -- returns an assignment that is a model of the BDD
 -- and maximises the sum of weights of variables.
--- The set of keys of the weight map *must* be the
--- full set of variables.
+-- Keys missing from the weight map, but present in the BDD,
+-- get weight zero.
 linopt :: ( Ord v , Num w, Ord w ) 
        => OBDD v 
        -> M.Map v w 
diff --git a/src/OBDD/Make.hs b/src/OBDD/Make.hs
--- a/src/OBDD/Make.hs
+++ b/src/OBDD/Make.hs
@@ -2,7 +2,7 @@
 
 module OBDD.Make 
 
-( constant, unit, variable, false, true )
+( constant, unit, variable )
 
 where
 
@@ -14,12 +14,6 @@
 constant :: Ord v => Bool -> OBDD v
 constant b = make $ do
     register $ Leaf b
-
-false :: Ord v => OBDD v
-false = constant False
-
-true :: Ord v => OBDD v
-true  = constant True
 
 -- | Variable with given parity
 unit :: Ord v => v -> Bool -> OBDD v
diff --git a/src/OBDD/Operation.hs b/src/OBDD/Operation.hs
--- a/src/OBDD/Operation.hs
+++ b/src/OBDD/Operation.hs
@@ -3,11 +3,12 @@
 
 module OBDD.Operation 
 
-( (&&), (||), not, and, or
-, ite, bool, implies, equiv, xor
+( Boolean(..)
+, equiv
 , unary, binary
 , instantiate
 , exists, exists_many
+, forall, forall_many
 , fold, foldM
 , full_fold, full_foldM
 )
@@ -16,6 +17,8 @@
 
 import OBDD.Data
 import OBDD.Make
+import Ersatz.Bit 
+import Data.Foldable (toList)
 
 import qualified Data.List ( sortBy)
 import Data.Function (on)
@@ -23,47 +26,24 @@
 import Data.Set ( Set )
 import qualified Data.Set as S
 
--- import Data.List ( foldl' )
--- don't use, see below
-
 import Prelude hiding ( (&&), (||), and, or, not, bool )
 import qualified Prelude
-
-infixr 3 &&
-
-( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v
-( && ) = symmetric_binary ( Prelude.&& )
-
-infixr 2 ||
-
-( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v
-( || ) = symmetric_binary ( Prelude.|| )
-
-bool :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v
-bool f t p = (f && not p) || (t && p)
+import qualified Data.Bool
 
-ite :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v
-ite i t e = bool e t i
+instance Ord v => Boolean (OBDD v) where
+  bool f = constant f
+  not = unary ( Prelude.not )
+  ( && ) = symmetric_binary ( Prelude.&& )
+  ( || ) = symmetric_binary ( Prelude.|| )
+  choose no yes sel = (no && not sel) || (yes && sel)
+  xor   = symmetric_binary (/=)
+  ( ==> ) = binary ( <= )
+  all p = fold_by_size (constant True ) (&&) . map p . toList
+  any p = fold_by_size (constant False) (||) . map p . toList
 
 equiv :: Ord v => OBDD v -> OBDD v -> OBDD v
 equiv = symmetric_binary (==)
 
-xor :: Ord v => OBDD v -> OBDD v -> OBDD v
-xor   = symmetric_binary (/=)
-
-implies :: Ord v => OBDD v -> OBDD v -> OBDD v
-implies = binary ( <= )
-
-and :: Ord v => [ OBDD v ] -> OBDD v
-and = fold_by_size (constant True) (&&)
--- and = foldr ( && ) ( constant True ) 
--- writing foldl or fold' here 
--- makes performance MUCH worse!
-
-or :: Ord v => [ OBDD v ] -> OBDD v
-or = fold_by_size (constant False) (||)
--- or = foldr ( || ) ( constant False ) 
-
 fold_by_size base reduce fs =
     let handle fs = case fs of
             [] -> base
@@ -77,11 +57,6 @@
     in  handle $ Data.List.sortBy (compare `on` size) fs
 
 
--- | FIXME this is a silly implementation. Negation should be done
--- by switching values in Leaves (?)
-not :: Ord v => OBDD v -> OBDD v 
-not = unary ( Prelude.not )
-
 unary :: Ord v 
       => ( Bool -> Bool )
       -> OBDD v -> OBDD v
@@ -138,44 +113,43 @@
                             register $ Branch v l' r'
     handle x y
 
+comp x y = case (x , y) of
+    ( Leaf {} , Leaf {} ) -> EQ
+    ( Branch {} , Leaf {} ) -> GT
+    ( Leaf {} , Branch {} ) ->  LT
+    ( Branch v1 _ _ , Branch v2 _ _ ) -> compare v1 v2
+
 -- | remove variables existentially
--- TODO: needs better implementation
-exists_many :: Ord v 
-            => Set v
+exists_many :: (Foldable c, Ord v)
+            => c v
             -> OBDD v
             -> OBDD v
 exists_many vars x =
-    foldr exists x $ S.toList vars 
+    foldr exists x vars 
 
 -- | remove variable existentially
--- TODO: needs better implementation
 exists :: Ord v
       => v
       -> OBDD v -> OBDD v
-exists var x = 
-    instantiate var False x || instantiate var True x
+exists var = fold bool
+  ( \ v l r -> if var == v then l || r else choose l r (variable v) )
 
+forall_many :: (Foldable c, Ord v) => c v -> OBDD v -> OBDD v
+forall_many vars x = 
+    foldr forall x vars 
+
+forall :: Ord v => v -> OBDD v -> OBDD v
+forall var = fold bool
+  ( \ v l r -> if var == v then l && r else choose l r (variable v) )
+
 -- | replace variable by value
 instantiate :: Ord v => 
             v -> Bool 
             -> OBDD v
             -> OBDD v
-instantiate var val x = make $ do
-    let handle x = cached ( top x, top x ) $ case access x of
-            Leaf p -> register $ Leaf p
-            Branch v l r -> 
-                if v == var then do
-                     let t = if val then r else l
-                     handle t
-                else  do
-                     l' <- handle l
-                     r' <- handle r
-                     register $ Branch v l' r' 
-    handle x
+instantiate var val = fold bool
+  ( \ v l r ->
+    if var == v then Data.Bool.bool l r val
+    else choose l r (variable v) )
 
-comp x y = case (x , y) of
-    ( Leaf {} , Leaf {} ) -> EQ
-    ( Branch {} , Leaf {} ) -> GT
-    ( Leaf {} , Branch {} ) ->  LT
-    ( Branch v1 _ _ , Branch v2 _ _ ) -> compare v1 v2
     
diff --git a/src/OBDD/Property.hs b/src/OBDD/Property.hs
--- a/src/OBDD/Property.hs
+++ b/src/OBDD/Property.hs
@@ -2,7 +2,7 @@
 
 ( null, satisfiable
 , number_of_models
-, some_model, all_models
+, paths, models
 , size
 )