diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Hiromi ISHII (c) 2019
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Hiromi ISHII nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/equational-reasoning-induction.cabal b/equational-reasoning-induction.cabal
new file mode 100644
--- /dev/null
+++ b/equational-reasoning-induction.cabal
@@ -0,0 +1,43 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.1.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 5489f953e454b40148d9ac7899bec3030961040eab5b3cf31f5b6d18f2efe6ba
+
+name:           equational-reasoning-induction
+version:        0.6.0.0
+synopsis:       Proof assistant for Haskell using DataKinds & PolyKinds
+description:    A simple convenient library to write equational / preorder proof as in Agda. This package depends on @singletons@ and generates induction schemes.
+category:       Math
+author:         Hiromi ISHII
+maintainer:     konn.jinro_at_gmail.com
+copyright:      (c) Hiromi ISHII 2013-2018
+license:        BSD3
+license-file:   LICENSE
+tested-with:    GHC==8.0.2 GHC==8.2.2 GHC==8.4.1 GHC==8.6.3
+build-type:     Simple
+
+source-repository head
+  type: git
+  location: git://github.com/konn/equational-reasoning-induction.git
+
+library
+  exposed-modules:
+      Proof.Induction
+  other-modules:
+      Proof.Internal.THCompat
+      Paths_equational_reasoning_induction
+  hs-source-dirs:
+      src
+  ghc-options: -Wall
+  build-depends:
+      base >=4 && <5
+    , singletons
+    , template-haskell >=2.11 && <2.16
+    , th-extras ==0.0.*
+  if impl(ghc <8.4)
+    build-depends:
+        semigroups ==0.18.*
+  default-language: Haskell2010
diff --git a/src/Proof/Induction.hs b/src/Proof/Induction.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Induction.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleContexts, GADTs #-}
+{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies   #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns      #-}
+module Proof.Induction (genInduction) where
+import Proof.Internal.THCompat
+
+import Control.Monad           (forM, replicateM)
+import Data.Either             (rights)
+import Data.Singletons.Prelude (Sing)
+import Language.Haskell.TH     (Clause, Con (ForallC, InfixC, NormalC, RecC))
+import Language.Haskell.TH     (TypeQ, appT, appsE, arrowT)
+import Language.Haskell.TH     (clause, conP, cxt, forallT)
+import Language.Haskell.TH     (funD, mkName, nameBase, newName)
+import Language.Haskell.TH     (normalB, promotedT, reify)
+import Language.Haskell.TH     (sigD, varE, varP, varT)
+import Language.Haskell.TH     (Dec, Info (TyConI), Name, Q)
+import Language.Haskell.TH     (Type (AppT, ConT, PromotedT, SigT))
+import Language.Haskell.TH.Lib (plainTV)
+
+-- | @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 -> DataDCompat _ 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 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
+
+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@DataDCompat {} = d
+normalizeDec (NewtypeDCompat ctx name tvbs con names) = mkDataD ctx name tvbs [con] names
+normalizeDec _ = error "not data definition."
diff --git a/src/Proof/Internal/THCompat.hs b/src/Proof/Internal/THCompat.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Internal/THCompat.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE CPP, PatternSynonyms, TemplateHaskell, ViewPatterns #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
+module Proof.Internal.THCompat where
+import Language.Haskell.TH
+import Language.Haskell.TH.Extras
+
+import GHC.Exts (Constraint)
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802
+import GHC.Generics
+import Data.Data
+#endif
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802
+data DerivClause = DerivClause (Maybe DerivStrategy) Cxt
+                 deriving (Eq, Data, Ord, Show, Generic)
+data  DerivStrategy = StockStrategy
+                    | AnyclassStrategy
+                    | NewtypeStrategy
+                    deriving (Eq, Data, Ord, Show, Generic)
+#endif
+
+dcToNames :: DerivClause -> [Name]
+dcToNames (DerivClause _ ct) = map headOfType ct
+
+dcToCxt :: DerivClause -> Cxt
+dcToCxt (DerivClause _ ct) = ct
+
+
+mkDataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec
+mkDataD ctx name tvbndrs cons dc =
+  DataD ctx name tvbndrs
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+        Nothing cons 
+#if __GLASGOW_HASKELL__ < 802
+        (concatMap dcToCxt dc)
+#else
+        dc
+#endif
+#else
+        cons (concatMap dcToNames dc)
+#endif
+
+
+typeName :: Type -> Name
+typeName (VarT n) = n
+typeName (ConT n) = n
+typeName (PromotedT n) = n
+typeName (TupleT n) = tupleTypeName n
+typeName (UnboxedTupleT n) = unboxedTupleTypeName n
+typeName ArrowT = ''(->)
+typeName EqualityT = ''(~)
+typeName ListT = ''[]
+typeName (PromotedTupleT n) = tupleDataName n
+typeName PromotedNilT = '[]
+typeName PromotedConsT = '(:)
+typeName ConstraintT = ''Constraint
+typeName _ = error "No names!"
+
+pattern DataDCompat :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec
+pattern DataDCompat ctx name tvbndrs cons dcs <-
+  DataD ctx name tvbndrs
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+        _ cons 
+#if __GLASGOW_HASKELL__ < 802
+        (pure . DerivClause Nothing -> dcs)
+#else 
+        dcs
+#endif
+#else
+        cons (DerivClause Nothing . map ConT -> dc)
+#endif
+
+pattern NewtypeDCompat :: Cxt -> Name -> [TyVarBndr] -> Con -> [DerivClause] -> Dec
+pattern NewtypeDCompat ctx name tvbndrs con dcs <-
+  NewtypeD ctx name tvbndrs
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+        _ con
+#if __GLASGOW_HASKELL__ < 802
+        (pure . DerivClause Nothing -> dcs)
+#else
+        dcs
+#endif
+#else
+        con
+        (DerivClause Nothing . map ConT -> dcs)
+#endif