diff --git a/Helper.hs b/Helper.hs
--- a/Helper.hs
+++ b/Helper.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE CPP #-}
 {-# OPTIONS -fno-warn-overlapping-patterns #-}
 module Helper where
     
@@ -13,7 +14,15 @@
                                        (x,y) -> (cxt++x,y)
 decomposeForallT t = ([],t)
 
+#if __GLASGOW_HASKELL__ >= 700
+classI_dec (ClassI x _ ) = x 
+#else
+classI_dec (ClassI x ) = x 
+#endif
+classI_dec info = error ("expected ClassI, got "++show info)
+                         
 
+
 lemma :: Name -> Name -> Q [Dec]
 lemma cls prf = do
         prfInfo <- reify prf
@@ -24,9 +33,7 @@
                     _ -> error ("expected ValI, got "++show prfInfo)
 
         info <- reify cls
-        let methodId = case info of
-                         ClassI (ClassD _ _ _ _ [SigD x _]) -> x
-                         _ -> error ("expected ClassI, got "++show info)
+        let methodId = (\(ClassD _ _ _ _ [SigD x _]) -> x) (classI_dec info)
                              
             (cxt,bodyT) = decomposeForallT typ
 
diff --git a/Type/Function.hs b/Type/Function.hs
--- a/Type/Function.hs
+++ b/Type/Function.hs
@@ -174,6 +174,7 @@
 domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2
 domUniq f f' = SetEq (domUniq0 f f') (domUniq0 f' f)
     where
+      domUniq0 :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :⊆: dom2
       domUniq0 f f' = Subset (\a -> case total f a of
                                      ExSnd fa -> inDom f' fa)
                                                   
diff --git a/Type/Logic.hs b/Type/Logic.hs
--- a/Type/Logic.hs
+++ b/Type/Logic.hs
@@ -36,11 +36,12 @@
 --
 module Type.Logic where
     
+import Control.Exception
+import Control.Monad.Trans.Cont
+import Data.Functor.Identity
+import Data.Monoid hiding(All)
 import Data.Type.Equality
-import Control.Monad.Cont
 import Data.Typeable
-import Data.Monoid hiding(All)
-import Control.Exception
 
     
 -- class Prop p where
@@ -238,10 +239,10 @@
 type COr r a b = Cont r (Either a b)
 
 lem :: COr r (a -> r) a
-lem = Cont (\k -> k (Left (\a -> k (Right a))))
+lem = ContT (\k -> k (Left (\a -> (runIdentity . k . Right) a)))
 
 elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r
-elimCor (Cont x) k1 k2 = x (either k1 k2) 
+elimCor (ContT x) k1 k2 = (runIdentity . x) (Identity . either k1 k2) 
                        
 
 
diff --git a/type-settheory.cabal b/type-settheory.cabal
--- a/type-settheory.cabal
+++ b/type-settheory.cabal
@@ -1,5 +1,5 @@
 name:                type-settheory
-version:             0.1.3
+version:             0.1.3.1
 synopsis:            
  Sets and functions-as-relations in the type system
 description:         
@@ -15,7 +15,7 @@
  .
  The proposition-types (derived from the ':=:' equality type) aren't meaningful purely by convention; they relate to the rest of Haskell as follows: A proof of @A :=: B@ gives us a safe coercion operator @A -> B@ (while the logic is inevitably inconsistent /at compile-time/ since 'undefined' proves anything, I think that we still have the property that if the 'Refl' value is successfully pattern-matched, then the two parameters in its type are actually equal). 
  
-category:            Math, Language
+category:            Math,Language,Type System
 license:             BSD3
 license-file:        LICENSE
 author:              Daniel Schüssler
@@ -33,7 +33,7 @@
                      , syb
                      , type-equality
                      , template-haskell
-                     , mtl
+                     , transformers
                      , containers
  exposed-modules:    Type.Logic
                      Type.Set