diff --git a/OBDD.hs b/OBDD.hs
deleted file mode 100644
--- a/OBDD.hs
+++ /dev/null
@@ -1,24 +0,0 @@
--- | reduced ordered binary decision diagrams
--- (c) Johannes Waldmann, 2008
---
--- this module is intended to be imported qualified
--- because it overloads some Prelude names.
---
--- for a similar, but much more elaborate project, see
--- <http://www.informatik.uni-kiel.de/~mh/lehre/diplomarbeiten/christiansen.pdf>
--- but I'm not sure where that source code would be available.
-
-module OBDD 
-
-( OBDD 
-, module OBDD.Property
-, module OBDD.Operation
-, module OBDD.Make
-) 
-
-where
-
-import OBDD.Data ( OBDD )
-import OBDD.Property
-import OBDD.Operation
-import OBDD.Make
diff --git a/OBDD/Data.hs b/OBDD/Data.hs
deleted file mode 100644
--- a/OBDD/Data.hs
+++ /dev/null
@@ -1,197 +0,0 @@
-{-# language GeneralizedNewtypeDeriving #-}
-
--- | implementation of reduced ordered binary decision diagrams.
-
-module OBDD.Data 
-
-(
--- * the data type
- OBDD -- abstract
--- * for external use
-, null, satisfiable
-, number_of_models
-, some_model, all_models
--- * for internal use
-, Node (..)
-, make
-, register
-, cached, top
-, access
-
-)
-
-where
-
-import Data.Map ( Map )
-import qualified Data.Map as M
-
-import Data.Set ( Set )
-import qualified Data.Set as S
-
-import Control.Monad.State
-import qualified System.Random
-
-import Prelude hiding ( null )
-import qualified Prelude
-
-newtype Index = Index Int deriving ( Eq, Ord, Num, Enum, Show )
-
--- | assumes total ordering on variables
-data OBDD v = OBDD
-	    { core :: Map Index ( Node v Index )
-	    , icore :: Map ( Node v Index ) Index
-	    , counter :: Map Index Integer -- ^ number of assignments
-	    , next :: Index
-	    , top :: Index
-	    , cache :: Map ( Index, Index ) Index -- ^ inputs and output for binary op
-		    -- (unary will be simulated by binary)
-	    }
-
--- | Number of satisfying assignments with  given set of variables.
--- The set of variables must be given since the current OBDD may not contain
--- all variables that were used to construct it, since some  nodes may have been removed
--- because they had identical children.
-number_of_models :: Ord v => Set v -> OBDD v ->  Integer
-number_of_models vs o = 
-    let fun o vs = do
-            m <- get
-            case access o of
-                   Leaf c -> case c of
-                        False -> return 0
-                        True -> return $ 2 ^ length vs
-                   Branch v l r -> do
-                       let ( pre, _ : post ) = span (/= v) vs
-                       case M.lookup ( top o ) m of
-                          Just x -> return $ ( 2 ^ length pre ) * x
-                          Nothing -> do
-                             xl <- fun l post
-                             xr <- fun r post
-                             let xlr = xl + xr
-                             m <- get
-                             put $ M.insert ( top o ) xlr m
-                             return $ ( 2 ^ length pre ) * xlr
-    in evalState ( fun o $ reverse $ S.toAscList vs ) M.empty
-    
-
-empty :: OBDD v
-empty = OBDD 
-      { core = M.empty
-      , icore = M.empty
-      , counter = M.empty
-      , next = 0
-      , top = error "OBDD.Data.empty"
-      , cache = M.empty
-      }
-
-data Node v i = Leaf Bool
-	    | Branch v i i
-    deriving ( Eq, Ord )
-
-{-! for Node derive: ToDoc !-}
-
-access :: OBDD v -> Node v ( OBDD v )
-access s = case M.lookup ( top s ) ( core s ) of
-    Nothing -> error "OBDD.Data.access"
-    Just n  -> case n of
-        Leaf p -> Leaf p
-	Branch v l r -> Branch v ( s { top = l } ) ( s { top = r } )
-
-count :: OBDD v -> Index -> Integer
-count s i = case M.lookup i ( counter s ) of
-    Nothing -> error "OBDD.Data.count"
-    Just n  -> n
-
--- | does the OBDD have any models?
-satisfiable :: OBDD v -> Bool
-satisfiable s = 0 < count s ( top s )
-
--- | does the OBDD not have any models?
-null :: OBDD v -> Bool
-null s = 0 == count s ( top s )
-
-
--- | randomly select one model, if possible
-some_model :: Ord v => OBDD v -> IO ( Maybe  ( Map v Bool ) )
-some_model s = case access s of
-    Leaf True -> return $ Just $ M.empty
-    Leaf False -> return Nothing
-    Branch v l r -> do
-        let nonempty_children = do
-                 ( p, t ) <- [ (False, l), (True, r) ]        
-                 guard $ case access t of
-                      Leaf False -> False
-                      _ -> True
-                 return ( p, t )
-        (p, t) <- select_one nonempty_children
-        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 s = case access s of
-    Leaf True -> return  M.empty
-    Leaf False -> [ ]
-    Branch v l r -> do
-        let nonempty_children = do
-                 ( p, t ) <- [ (False, l), (True, r) ]        
-                 guard $ case access t of
-                      Leaf False -> False
-                      _ -> True
-                 return ( p, t )
-        (p, t) <- nonempty_children
-        m <- all_models t
-        return $ M.insert v p m 
-        
-select_one :: [a] -> IO a
-select_one xs | not ( Prelude.null xs ) = do
-    i <- System.Random.randomRIO ( 0, length xs - 1 )
-    return $ xs !! i
-
-make :: State ( OBDD v ) Index
-     -> OBDD v
-make action = 
-    let ( i, s ) = runState action empty 
-    in  s { top = i }
-
-fresh :: State ( OBDD v ) Index
-fresh = do
-    s <- get
-    let i = next s
-    put $ s { next = succ i }
-    return i
-
-cached :: Ord v
-	=> (Index, Index) 
-	-> ( State ( OBDD v ) Index )
-	-> State ( OBDD v ) Index
-cached (l,r) action = do
-    s <- get
-    case M.lookup (l,r) $ cache s of
-        Just i -> return i
-	Nothing -> do
-	    i <- action
-	    s <- get
-	    put $ s { cache = M.insert ( l,r) i $ cache s }
-	    return i
-
-register :: Ord v
-	 => Node v Index
-       -> State ( OBDD v ) Index
-register n = do
-    s <- get
-    case M.lookup n ( icore s ) of
-        Just i -> return i
-	Nothing -> case n of
-            Branch v l r | l == r -> return l -- TRICK (?)
-            _ -> do
-	        i <- fresh
-	        s <- get
-	        let c = case n of
-		        Leaf p -> if p then 1 else 0
-		        Branch v l r -> count s l + count s r 
-	        put $ s 
-		    { core = M.insert i n $ core s
-		    , icore = M.insert n i $ icore s
-		    , counter = M.insert i c $ counter s
-		    }
-	        return i  
diff --git a/OBDD/Make.hs b/OBDD/Make.hs
deleted file mode 100644
--- a/OBDD/Make.hs
+++ /dev/null
@@ -1,24 +0,0 @@
--- | builds basic OBDDs
-
-module OBDD.Make 
-
-( constant, unit )
-
-where
-
-import OBDD.Data
-
-import Data.Map ( Map )
-import qualified Data.Map as M
-
-constant :: Ord v => Bool -> OBDD v
-constant b = make $ do
-    register $ Leaf b
-
--- | Variable with given parity
-unit :: Ord v => v -> Bool -> OBDD v
-unit v p = make $ do
-    l <- register $ Leaf $ not p
-    r <- register $ Leaf $     p
-    register $ Branch v l r
-
diff --git a/OBDD/Operation.hs b/OBDD/Operation.hs
deleted file mode 100644
--- a/OBDD/Operation.hs
+++ /dev/null
@@ -1,123 +0,0 @@
-{-# language ScopedTypeVariables #-}
-
-module OBDD.Operation 
-
-( (&&), (||), not, and, or
-, unary, binary
-, instantiate
-, exists, exists_many
-)
-
-where
-
-import OBDD.Data
-import OBDD.Make
-
-import Data.Map ( Map )
-import qualified Data.Map as M
-
-import Data.Set ( Set )
-import qualified Data.Set as S
-
-import Prelude hiding ( (&&), (||), and, or, not )
-import qualified Prelude
-
-( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v
-( && ) = binary ( Prelude.&& )
-
-( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v
-( || ) = binary ( Prelude.|| )
-
-and :: Ord v => [ OBDD v ] -> OBDD v
-and = foldr ( && ) ( constant True ) 
-
-or :: Ord v => [ OBDD v ] -> OBDD v
-or = foldr ( || ) ( constant False ) 
-
-
--- | 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
-unary op x = make $ do
-    let handle x = cached ( top x, top x ) $ case access x of
-	        Leaf p -> register $ Leaf $ op p
-		Branch v l r -> do
-			l' <- handle l
-			r' <- handle r
-			register $ Branch v l' r'
-    handle x
-
-
-binary :: Ord v
-      => ( Bool -> Bool -> Bool )
-      -> OBDD v -> OBDD v -> OBDD v
-binary op x y = make $ do
-    let handle x y = cached (top x, top y) $ case ( access x , access y ) of
-	            ( Leaf p , Leaf q ) -> register $ Leaf $ op p q
-		    ( ax, ay ) -> case comp ax ay of
-		        LT -> do
-		            let Branch v l r = ay
-			    l' <- handle x l
-			    r' <- handle x r
-			    register $ Branch v l' r'
-			GT -> do
-			    let Branch v l r = ax
-			    l' <- handle l y
-			    r' <- handle r y
-			    register $ Branch v l' r'
-			EQ -> do
-			    let Branch v1 l1 r1 = ax
-				Branch v2 l2 r2 = ay
-				v = if v1 == v2 then v1 else error "OBDD.Operation.handle"
-			    l' <- handle l1 l2
-			    r' <- handle r1 r2
-			    register $ Branch v l' r'
-    handle x y
-
--- | remove variables existentially
--- TODO: needs better implementation
-exists_many :: Ord v 
-            => Set v
-            -> OBDD v
-            -> OBDD v
-exists_many vars x =
-    foldr exists x $ S.toList 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
-
--- | 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
-
-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/OBDD/Property.hs b/OBDD/Property.hs
deleted file mode 100644
--- a/OBDD/Property.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-module OBDD.Property 
-
-( null, satisfiable
-, number_of_models
-, some_model, all_models
-)
-
-where
-
-import qualified Prelude
-import OBDD.Data
-
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,1 @@
+module Main (main) where import Distribution.Simple ; main = defaultMain
diff --git a/Setup.lhs b/Setup.lhs
deleted file mode 100644
--- a/Setup.lhs
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/local/bin/runhaskell
-
-> import Distribution.Simple
-> main = defaultMain
-
diff --git a/obdd.cabal b/obdd.cabal
--- a/obdd.cabal
+++ b/obdd.cabal
@@ -1,12 +1,24 @@
 Name:                obdd
-Version:             0.2
+Version:             0.2.3
+Cabal-Version:       >= 1.6
+Build-type: Simple
 Synopsis:            Ordered Reduced Binary Decision Diagrams
 Description:         Construct, combine and query OBDDs;
                      an efficient representation for formulas in propositional logic
+category:	     Logic
 License:             GPL
 License-file:        LICENSE
 Author:              Johannes Waldmann
 Maintainer:          Johannes Waldmann <waldmann@imn.htwk-leipzig.de>
-Build-Depends:       base, random, mtl, containers
-Build-Type:	     Simple
-Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property
+
+library
+    Build-Depends:       base==4.*, random, mtl, containers
+    Hs-Source-Dirs:	     src
+    Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property
+    ghc-options: -funbox-strict-fields
+
+
+Source-Repository head
+    Type: git
+    Location: git://dfa.imn.htwk-leipzig.de/srv/git/obdd/
+
diff --git a/src/OBDD.hs b/src/OBDD.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD.hs
@@ -0,0 +1,24 @@
+-- | reduced ordered binary decision diagrams
+-- (c) Johannes Waldmann, 2008
+--
+-- this module is intended to be imported qualified
+-- because it overloads some Prelude names.
+--
+-- for a similar, but much more elaborate project, see
+-- <http://www.informatik.uni-kiel.de/~mh/lehre/diplomarbeiten/christiansen.pdf>
+-- but I'm not sure where that source code would be available.
+
+module OBDD 
+
+( OBDD 
+, module OBDD.Property
+, module OBDD.Operation
+, module OBDD.Make
+) 
+
+where
+
+import OBDD.Data ( OBDD )
+import OBDD.Property
+import OBDD.Operation
+import OBDD.Make
diff --git a/src/OBDD/Data.hs b/src/OBDD/Data.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD/Data.hs
@@ -0,0 +1,202 @@
+{-# language GeneralizedNewtypeDeriving #-}
+
+-- | implementation of reduced ordered binary decision diagrams.
+
+module OBDD.Data 
+
+(
+-- * the data type
+ OBDD -- abstract
+, size
+-- * for external use
+, null, satisfiable
+, number_of_models
+, some_model, all_models
+-- * for internal use
+, Node (..)
+, make
+, register
+, cached, top
+, access
+
+)
+
+where
+
+import Data.Map.Strict ( Map )
+import qualified Data.Map.Strict as M
+
+import Data.Set ( Set )
+import qualified Data.Set as S
+
+import Control.Monad.State.Strict
+import qualified System.Random
+
+import Prelude hiding ( null )
+import qualified Prelude
+
+newtype Index = Index { unIndex :: Int }
+   deriving ( Eq, Ord, Num, Enum, Show )
+
+-- | assumes total ordering on variables
+data OBDD v = OBDD
+	    { core :: !(Map Index ( Node v Index ))
+	    , icore :: !(Map ( Node v Index ) Index)
+	    , counter :: Map Index Integer -- ^ number of assignments
+	    , next :: !Index
+	    , top :: !Index
+	    , cache :: ! (Map ( Index, Index ) Index) -- ^ inputs and output for binary op
+		    -- (unary will be simulated by binary)
+	    }
+
+size = unIndex . next
+
+-- | Number of satisfying assignments with  given set of variables.
+-- The set of variables must be given since the current OBDD may not contain
+-- all variables that were used to construct it, since some  nodes may have been removed
+-- because they had identical children.
+number_of_models :: Ord v => Set v -> OBDD v ->  Integer
+number_of_models vs o = 
+    let fun o vs = do
+            m <- get
+            case access o of
+                   Leaf c -> case c of
+                        False -> return 0
+                        True -> return $ 2 ^ length vs
+                   Branch v l r -> do
+                       let ( pre, _ : post ) = span (/= v) vs
+                       case M.lookup ( top o ) m of
+                          Just x -> return $ ( 2 ^ length pre ) * x
+                          Nothing -> do
+                             xl <- fun l post
+                             xr <- fun r post
+                             let xlr = xl + xr
+                             m <- get
+                             put $ M.insert ( top o ) xlr m
+                             return $ ( 2 ^ length pre ) * xlr
+    in evalState ( fun o $ reverse $ S.toAscList vs ) M.empty
+    
+
+empty :: OBDD v
+empty = OBDD 
+      { core = M.empty
+      , icore = M.empty
+      , counter = M.empty
+      , next = 0
+      , top = -42 -- error "OBDD.Data.empty"
+      , cache = M.empty
+      }
+
+data Node v i = Leaf !Bool
+	    | Branch !v !i !i
+    deriving ( Eq, Ord )
+
+{-! for Node derive: ToDoc !-}
+
+access :: OBDD v -> Node v ( OBDD v )
+access s = case M.lookup ( top s ) ( core s ) of
+    Nothing -> error "OBDD.Data.access"
+    Just n  -> case n of
+        Leaf p -> Leaf p
+	Branch v l r -> 
+          Branch v ( s { top = l } ) ( s { top = r } )
+
+count :: OBDD v -> Index -> Integer
+count s i = case M.lookup i ( counter s ) of
+    Nothing -> error "OBDD.Data.count"
+    Just n  -> n
+
+-- | does the OBDD have any models?
+satisfiable :: OBDD v -> Bool
+satisfiable s = 0 < count s ( top s )
+
+-- | does the OBDD not have any models?
+null :: OBDD v -> Bool
+null s = 0 == count s ( top s )
+
+
+-- | randomly select one model, if possible
+some_model :: Ord v => OBDD v -> IO ( Maybe  ( Map v Bool ) )
+some_model s = case access s of
+    Leaf True -> return $ Just $ M.empty
+    Leaf False -> return Nothing
+    Branch v l r -> do
+        let nonempty_children = do
+                 ( p, t ) <- [ (False, l), (True, r) ]        
+                 guard $ case access t of
+                      Leaf False -> False
+                      _ -> True
+                 return ( p, t )
+        (p, t) <- select_one nonempty_children
+        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 s = case access s of
+    Leaf True -> return  M.empty
+    Leaf False -> [ ]
+    Branch v l r -> do
+        let nonempty_children = do
+                 ( p, t ) <- [ (False, l), (True, r) ]        
+                 guard $ case access t of
+                      Leaf False -> False
+                      _ -> True
+                 return ( p, t )
+        (p, t) <- nonempty_children
+        m <- all_models t
+        return $ M.insert v p m 
+        
+select_one :: [a] -> IO a
+select_one xs | not ( Prelude.null xs ) = do
+    i <- System.Random.randomRIO ( 0, length xs - 1 )
+    return $ xs !! i
+
+make :: State ( OBDD v ) Index
+     -> OBDD v
+make action = 
+    let ( i, s ) = runState action empty 
+    in  i `seq` s { top = i }
+
+fresh :: State ( OBDD v ) Index
+fresh = do
+    s <- get
+    let i = next s
+    put $ s { next = succ i }
+    return i
+
+cached :: Ord v
+	=> (Index, Index) 
+	-> ( State ( OBDD v ) Index )
+	-> State ( OBDD v ) Index
+cached (l,r) action = do
+    s <- get
+    case M.lookup (l,r) $ cache s of
+        Just i -> return i
+	Nothing -> do
+	    i <- action
+	    s <- get
+	    put $ s { cache = M.insert ( l,r) i $ cache s }
+	    return i
+
+register :: Ord v
+	 => Node v Index
+       -> State ( OBDD v ) Index
+register n = do
+    s <- get
+    case M.lookup n ( icore s ) of
+        Just i -> return i
+	Nothing -> case n of
+            Branch v l r | l == r -> return l -- TRICK (?)
+            _ -> do
+	        i <- fresh
+	        s <- get
+	        let c = case n of
+		        Leaf p -> if p then 1 else 0
+		        Branch v l r -> count s l + count s r 
+	        put $ s 
+		    { core = M.insert i n $ core s
+		    , icore = M.insert n i $ icore s
+		    , counter = M.insert i c $ counter s
+		    }
+	        return i  
diff --git a/src/OBDD/Make.hs b/src/OBDD/Make.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD/Make.hs
@@ -0,0 +1,24 @@
+-- | builds basic OBDDs
+
+module OBDD.Make 
+
+( constant, unit )
+
+where
+
+import OBDD.Data
+
+import Data.Map ( Map )
+import qualified Data.Map as M
+
+constant :: Ord v => Bool -> OBDD v
+constant b = make $ do
+    register $ Leaf b
+
+-- | Variable with given parity
+unit :: Ord v => v -> Bool -> OBDD v
+unit v p = make $ do
+    l <- register $ Leaf $ not p
+    r <- register $ Leaf $     p
+    register $ Branch v l r
+
diff --git a/src/OBDD/Operation.hs b/src/OBDD/Operation.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD/Operation.hs
@@ -0,0 +1,125 @@
+{-# language ScopedTypeVariables #-}
+
+module OBDD.Operation 
+
+( (&&), (||), not, and, or
+, unary, binary
+, instantiate
+, exists, exists_many
+)
+
+where
+
+import OBDD.Data
+import OBDD.Make
+
+import Data.Map ( Map )
+import qualified Data.Map as M
+
+import Data.Set ( Set )
+import qualified Data.Set as S
+
+import Data.List ( foldl' )
+
+import Prelude hiding ( (&&), (||), and, or, not )
+import qualified Prelude
+
+( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v
+( && ) = binary ( Prelude.&& )
+
+( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v
+( || ) = binary ( Prelude.|| )
+
+and :: Ord v => [ OBDD v ] -> OBDD v
+and = foldl' ( && ) ( constant True ) 
+
+or :: Ord v => [ OBDD v ] -> OBDD v
+or = foldl' ( || ) ( constant False ) 
+
+
+-- | 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
+unary op x = make $ do
+    let handle x = cached ( top x, top x ) $ case access x of
+	        Leaf p -> register $ Leaf $ op p
+		Branch v l r -> do
+			l' <- handle l
+			r' <- handle r
+			register $ Branch v l' r'
+    handle x
+
+
+binary :: Ord v
+      => ( Bool -> Bool -> Bool )
+      -> OBDD v -> OBDD v -> OBDD v
+binary op x y = make $ do
+    let handle x y = cached (top x, top y) $ case ( access x , access y ) of
+	            ( Leaf p , Leaf q ) -> register $ Leaf $ op p q
+		    ( ax, ay ) -> case comp ax ay of
+		        LT -> do
+		            let Branch v l r = ay
+			    l' <- handle x l
+			    r' <- handle x r
+			    register $ Branch v l' r'
+			GT -> do
+			    let Branch v l r = ax
+			    l' <- handle l y
+			    r' <- handle r y
+			    register $ Branch v l' r'
+			EQ -> do
+			    let Branch v1 l1 r1 = ax
+				Branch v2 l2 r2 = ay
+				v = if v1 == v2 then v1 else error "OBDD.Operation.handle"
+			    l' <- handle l1 l2
+			    r' <- handle r1 r2
+			    register $ Branch v l' r'
+    handle x y
+
+-- | remove variables existentially
+-- TODO: needs better implementation
+exists_many :: Ord v 
+            => Set v
+            -> OBDD v
+            -> OBDD v
+exists_many vars x =
+    foldr exists x $ S.toList 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
+
+-- | 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
+
+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
new file mode 100644
--- /dev/null
+++ b/src/OBDD/Property.hs
@@ -0,0 +1,12 @@
+module OBDD.Property 
+
+( null, satisfiable
+, number_of_models
+, some_model, all_models
+)
+
+where
+
+import qualified Prelude
+import OBDD.Data
+