diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -32,10 +32,10 @@
 leibnizToRefl :: Leibniz a b -> a :=: b
 leibnizToRefl eq = apply eq Refl
 
-fromLeibniz :: (Preorder eq, SingRep a) => Leibniz a b -> eq a b
+fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b
 fromLeibniz eq = apply eq (reflexivity sing)
 
-fromRefl :: (Preorder eq, SingRep b) => a :=: b -> eq a b
+fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b
 fromRefl Refl = reflexivity'
 
 reflToLeibniz :: a :=: b -> Leibniz a b
@@ -76,7 +76,7 @@
 data Reason eq x y where
   Because :: Sing y -> eq x y -> Reason eq x y
 
-reflexivity' :: (SingRep x, Preorder r) => r x x
+reflexivity' :: (SingI x, Preorder r) => r x x
 reflexivity' = reflexivity sing
 
 by, because :: Sing y -> eq x y -> Reason eq x y
@@ -102,7 +102,7 @@
 start :: Preorder eq => Sing a -> eq a a
 start = reflexivity
 
-byDefinition :: (SingRep a, Preorder eq) => eq a a
+byDefinition :: (SingI a, Preorder eq) => eq a a
 byDefinition = reflexivity sing
 
 admitted :: Reason eq x y
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.0.4.1
+version:             0.1.0.0
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 description:         A simple convenient library to write equational / preorder proof as in Agda.
 license:             BSD3
@@ -21,8 +21,12 @@
 library
   exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction
   build-depends:       base             >= 4      && < 5
-               ,       singletons       == 0.8.*
-               ,       tagged           == 0.6.*
                ,       void             == 0.6.*
                ,       template-haskell >= 2.8    && < 2.11
+  if impl(ghc < 7.8)
+    build-depends:     singletons       == 0.8.*
+                 ,     tagged           >= 0.6
+  else
+    build-depends:     singletons       >= 0.8    && < 0.11
+