diff --git a/presburger.cabal b/presburger.cabal
--- a/presburger.cabal
+++ b/presburger.cabal
@@ -1,5 +1,5 @@
 Name:           presburger
-Version:        0.1
+Version:        0.2
 License:        BSD3
 License-file:   LICENSE
 Author:         Iavor S. Diatchki
diff --git a/src/Data/Integer/Presburger.hs b/src/Data/Integer/Presburger.hs
--- a/src/Data/Integer/Presburger.hs
+++ b/src/Data/Integer/Presburger.hs
@@ -79,8 +79,14 @@
 
 pre_ex :: (Bool,Int) -> [Name] -> Formula -> Form
 pre_ex (top,n) xs form = case form of
-  Exists f          -> pre_ex (top,n+1) (n:xs) (f (var (n+1)))
+  Exists f          -> pre_ex (top,n+1) (n:xs) (f (var n))
   f1 :\/: f2        -> or' (pre_ex (top,n) xs f1) (pre_ex (top,n) xs f2)
+  Not form1 ->
+    case form1 of
+      Not form2     -> pre_ex (top,n) xs form2
+      Forall f      -> pre_ex (top,n) xs (Exists (Not . f))
+      p :/\: q      -> pre_ex (top,n) xs (Not p :\/: Not q)
+      _             -> exists_many top xs (pre (False,n) form)
   _                 -> exists_many top xs (pre (False,n) form)
 
 invert :: Form -> Formula
@@ -114,7 +120,7 @@
 
 type Name           = Int
 
--- | @split_term x (n * x + t1) = (n,t1)
+-- | @split_term x (n * x + t1) = (n,t1)@
 -- @x@ does not occur in @t1@
 split_term         :: Name -> Term -> (Integer,Term)
 split_term x (Term m n) = (fromMaybe 0 c, Term m1 n)