diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -16,7 +16,7 @@
                           -- * Conversion between equalities
                         , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl
                           -- * Coercion
-                        , coerce, coerce'
+                        , coerce, coerce', withRefl
                           -- * Re-exported modules
                         , module Data.Singletons, module Data.Proxy
                         ) where
@@ -136,19 +136,31 @@
 -- Using this function instead of pattern-matching on equality proof,
 -- you can reduce the overhead introduced by run-time proof.
 coerce :: (a :=: b) -> f a -> f b
-coerce Refl a = unsafeCoerce a
+coerce _ a = unsafeCoerce a
 {-# INLINE[1] coerce #-}
 
 -- | Coercion for identity types.
 coerce' :: a :=: b -> a -> b
-coerce' Refl a = unsafeCoerce a
+coerce' _ a = unsafeCoerce a
 {-# INLINE[1] coerce' #-}
 
 {-# RULES
-"coerce/unsafeCoerce" forall xs.
+"coerce/unsafeCoerce" [~1] forall xs.
   coerce xs = unsafeCoerce
-"coerce'/unsafeCoerce" forall xs.
+"coerce'/unsafeCoerce" [~1] forall xs.
   coerce' xs = unsafeCoerce
+  #-}
+
+-- | Solves equality constraint without explicit coercion.
+--   It has the same effect as @'Data.Type.Equality.gcastWith'@,
+--   but some hacks is done to reduce runtime overhead.
+withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
+withRefl _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of
+  Refl -> r
+{-# INLINE [1] withRefl #-}
+{-# RULES
+"withRefl/unsafeCoerce" [~1] forall x.
+  withRefl x = unsafeCoerce
   #-}
 
 class Proposition (f :: k -> *) where
diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
--- a/Proof/Propositional.hs
+++ b/Proof/Propositional.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll     #-}
 {-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
 {-# LANGUAGE LambdaCase, PolyKinds, StandaloneDeriving, TemplateHaskell   #-}
-{-# LANGUAGE TypeOperators                                                #-}
+{-# LANGUAGE TypeOperators, RankNTypes                                    #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 -- | Provides type synonyms for logical connectives.
 module Proof.Propositional
@@ -22,6 +22,7 @@
 import Data.Type.Equality ((:~:))
 import Data.Typeable      (Typeable)
 import Data.Void
+import Unsafe.Coerce
 
 type a /\ b = (a, b)
 type a \/ b = Either a b
@@ -73,6 +74,14 @@
 data IsTrue (b :: Bool) where
   Witness :: IsTrue 'True
 
+withWitness :: IsTrue b -> (b ~ 'True => r) -> r
+withWitness Witness r = r
+{-# INLINE [1] withWitness #-}
+{-# RULES
+"withWitness/coercion" [~1] forall x.
+  withWitness x = unsafeCoerce
+  #-}
+
 deriving instance Show (IsTrue b)
 deriving instance Eq   (IsTrue b)
 deriving instance Ord  (IsTrue b)
@@ -85,6 +94,14 @@
 
 refute [t| 0 :~: 1 |]
 refute [t| () :~: Int |]
+refute [t| 'True :~: 'False |]
+refute [t| 'False :~: 'True |]
+refute [t| 'LT :~: 'GT |]
+refute [t| 'LT :~: 'EQ |]
+refute [t| 'EQ :~: 'LT |]
+refute [t| 'EQ :~: 'GT |]
+refute [t| 'GT :~: 'LT |]
+refute [t| 'GT :~: 'EQ |]
 
 prove [t| Bool |]
 prove [t| Int |]
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.4.0.0
+version:             0.4.1.0
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 description:         A simple convenient library to write equational / preorder proof as in Agda.
 license:             BSD3