diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -4,13 +4,18 @@
 module Proof.Equational ((:=:)(..), Equality(..), Preorder(..), reflexivity'
                         ,(:\/:), (:/\:), (=>=), (=~=), Leibniz(..)
                         , Reason(..), because, by, (===), start, byDefinition
-                        , admitted, Proxy(..), cong, cong', fromRefl
+                        , admitted, Proxy(..), cong, cong'
                         , Proposition(..), (:~>), FromBool (..)
+                          -- * Conversion between equalities
+                        , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl
+                          -- * Coercion
+                        , coerce, coerce'
                           -- * Re-exported modules
                         , module Data.Singletons, module Data.Proxy
                         ) where
 import Data.Proxy
 import Data.Singletons
+import Unsafe.Coerce
 
 infix 4 :=:
 type a :\/: b = Either a b
@@ -24,9 +29,18 @@
 
 data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }
 
+leibnizToRefl :: Leibniz a b -> a :=: b
+leibnizToRefl eq = apply eq Refl
+
+fromLeibniz :: (Preorder eq, SingRep a) => Leibniz a b -> eq a b
+fromLeibniz eq = apply eq (reflexivity sing)
+
 fromRefl :: (Preorder eq, SingRep b) => a :=: b -> eq a b
 fromRefl Refl = reflexivity'
 
+reflToLeibniz :: a :=: b -> Leibniz a b
+reflToLeibniz Refl = Leibniz id
+
 deriving instance Show (a :=: b)
 
 class Preorder (eq :: k -> k -> *) where
@@ -97,6 +111,19 @@
 
 cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b
 cong' _ Refl =  Refl
+
+-- | Type coercion. 'coerce' is using @unsafeCoerce a@.
+-- So, please, please do not provide the @undefined@ as the proof.
+-- 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
+{-# INLINE coerce #-}
+
+-- | Coercion for identity types.
+coerce' :: a :=: b -> a -> b
+coerce' Refl a = unsafeCoerce a
+{-# INLINE coerce' #-}
 
 class Proposition f where
   type OriginalProp f n :: *
diff --git a/Proof/Induction.hs b/Proof/Induction.hs
new file mode 100644
--- /dev/null
+++ b/Proof/Induction.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators              #-}
+{-# LANGUAGE UndecidableInstances, ViewPatterns                        #-}
+module Proof.Induction (genInduction) where
+import Control.Applicative
+import Control.Monad
+import Data.Char
+import Data.Either
+import Data.List
+import Data.Singletons
+import Language.Haskell.TH
+import Language.Haskell.TH.Lib
+
+capitalize :: String -> String
+capitalize (x :xs) = toUpper x : xs
+capitalize _ = error "capitalize"
+
+-- | @genInduction ''Type "inductionT"@ defines the induction scheme for @Type@ named @inductionT@.
+genInduction :: Name -> String -> Q [Dec]
+genInduction typ fname0 = do
+  let fname = mkName fname0
+  TyConI (normalizeDec -> DataD _ dName _ dCons _) <- reify typ
+  p <- newName "p"
+  ans <- mapM (buildCase fname (length dCons) dName p) $ zip [0..] dCons
+  let (cls, ts) = unzip ans
+  t <- newName "t"
+  sig <- sigD fname $ forallT [plainTV p, plainTV t] (cxt []) $
+           foldr toT ([t| Sing $(varT t) -> $(varT p) $(varT t) |]) $ map return ts
+  dec <- funD fname (map return cls)
+  return [sig, dec]
+
+buildCase :: Name -> Int -> Name -> Name -> (Int, Con) -> Q (Clause, Type)
+buildCase _ _ _ _ (_, ForallC _ _ _) = error "Existential types are not supported yet."
+buildCase fname size dName p (nth, dCon) = do
+  let paramTs = extractParams dCon
+      conName = extractName dCon
+      sName = mkName $ 'S' : nameBase conName
+      ssName = mkName $ 's' : nameBase conName
+  eparams <- forM paramTs $ \ty ->
+    case getTyConName ty of
+      Just nm | nm == dName -> Right <$> newName "t"
+      _ -> Left <$> newName "a"
+  xs <- replicateM (length paramTs) $ newName "x"
+  let freeVars = lefts eparams
+      subCases = [[t| Sing $(varT t) -> $(varT p) $(varT t) |] | t <- rights eparams ]
+  params <- mapM (either varT varT) eparams
+  let promCon = foldl appT (promotedT conName) (map return params)
+      tbdy | null subCases = foldr toT ([t| $(varT p `appT` promCon) |]) subCases
+           | otherwise   = foldr toT ([t| Sing $(promCon) -> $(varT p `appT` promCon) |]) subCases
+  sig <- if null params then tbdy else forallT (map (either plainTV plainTV) eparams) (cxt []) tbdy
+  cs <- replicateM size $ newName "case"
+  let body | null subCases = varE (cs !! nth)
+           | otherwise = appsE $ varE (cs !! nth) : 
+               replicate (length subCases) (appsE $ varE fname : map varE cs)
+               ++ [ appsE (varE ssName : map varE xs)]
+  cl <- clause (map varP cs ++ [conP sName $ map varP xs]) (normalB body) []
+  return (cl, sig)
+  where
+    extractName (NormalC n _) = n
+    extractName (RecC n _) = n
+    extractName (InfixC _ n _) = n
+    extractName _ = error "I don't know name!"
+    extractParams (NormalC _ sts) = map snd sts
+    extractParams (RecC _ vsts)   = map (\(_,_,c) -> c) vsts
+    extractParams (InfixC (_, t) _ (_, s)) = [t,s]
+    extractParams _ = []
+
+toT :: TypeQ -> TypeQ -> TypeQ
+a `toT` b = arrowT `appT` a `appT` b
+
+getFreeVarT :: Type -> [Name]
+getFreeVarT (AppT a b) = getFreeVarT a ++ getFreeVarT b
+getFreeVarT (SigT a _) = getFreeVarT a
+getFreeVarT (ForallT tvs _ t) = getFreeVarT t \\ map tyVarName tvs
+getFreeVarT (VarT n)   = [n]
+getFreeVarT _          = []
+
+tyVarName :: TyVarBndr -> Name
+tyVarName (PlainTV n) = n
+tyVarName (KindedTV n _) = n
+
+getTyConName :: Type -> Maybe Name
+getTyConName (AppT a _)    = getTyConName a
+getTyConName (SigT a _)    = getTyConName a
+getTyConName (ConT nam)    = Just nam
+getTyConName (PromotedT n) = Just n
+getTyConName _             = Nothing
+
+normalizeDec :: Dec -> Dec
+normalizeDec d@(DataD _ _ _ _ _) = d
+normalizeDec (NewtypeD ctx name tvbs con names) = DataD ctx name tvbs [con] names
+normalizeDec _ = error "not data definition."
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.1.0
+version:             0.0.3.0
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 -- description:         
 license:             BSD3
@@ -15,9 +15,10 @@
 cabal-version:       >=1.8
 
 library
-  exposed-modules:     Proof.Equational, Proof.Propositional
-  build-depends:       base       == 4.6.*
-               ,       singletons == 0.8.*
-               ,       tagged     == 0.6.*
-               ,       void       == 0.6.*
+  exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction
+  build-depends:       base             == 4.6.*
+               ,       singletons       == 0.8.*
+               ,       tagged           == 0.6.*
+               ,       void             == 0.6.*
+               ,       template-haskell == 2.8.*