diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -89,11 +89,17 @@
   symmetry     :: eq a b  -> eq b a
 
 instance Preorder (:=:) where
+  {-# SPECIALISE instance Preorder (:=:) #-}
   transitivity Refl Refl = Refl
+  {-# INLINE[1] transitivity #-}
+
   reflexivity  _         = Refl
+  {-# INLINE[1] reflexivity #-}
 
 instance Equality (:=:) where
+  {-# SPECIALISE instance Equality (:~:) #-}
   symmetry     Refl      = Refl
+  {-# INLINE[1] symmetry #-}
 
 instance Preorder (->) where
   reflexivity _ = id
@@ -128,11 +134,16 @@
 (=<=) :: Preorder r => r x y -> Reason r y z -> r x z
 eq =<= (_ `Because` eq') = transitivity eq eq'
 
+{-# SPECIALISE INLINE[1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
+
 (=>=) :: Preorder r => r y z -> Reason r x y -> r x z
 eq =>= (_ `Because` eq') = transitivity eq' eq
 
+{-# SPECIALISE INLINE[1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
+
 (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
 (===) = (=<=)
+{-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
 (=~=) :: Preorder r => r x y -> Sing y -> r x y
 eq =~= _ = eq
@@ -159,12 +170,20 @@
 -- you can reduce the overhead introduced by run-time proof.
 coerce :: (a :=: b) -> f a -> f b
 coerce Refl a = unsafeCoerce a
-{-# INLINE coerce #-}
+{-# INLINE[1] coerce #-}
 
 -- | Coercion for identity types.
 coerce' :: a :=: b -> a -> b
 coerce' Refl a = unsafeCoerce a
-{-# INLINE coerce' #-}
+{-# INLINE[1] coerce' #-}
+
+{-# RULES
+"coerce/unsafeCoerce" forall xs.
+  coerce xs = unsafeCoerce
+"coerce'/unsafeCoerce" forall xs.
+  coerce' xs = unsafeCoerce
+  #-}
+
 
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
 class Proposition (f :: k -> *) where
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.2.0.4
+version:             0.2.0.5
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 description:         A simple convenient library to write equational / preorder proof as in Agda.
 license:             BSD3
@@ -22,7 +22,7 @@
 library
   exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction
   build-depends:       base             >= 4      && < 5
-               ,       void             == 0.6.*
+               ,       void             >= 0.6    && < 0.8
                ,       template-haskell >= 2.8    && < 2.11
   if impl(ghc < 7.8)
     build-depends:     singletons       == 0.8.*