diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -18,10 +18,9 @@
                           -- * Coercion
                         , coerce, coerce', withRefl
                           -- * Re-exported modules
-                        , module Data.Singletons, module Data.Proxy
+                        , module Data.Proxy
                         ) where
 import Data.Proxy
-import Data.Singletons
 import Data.Type.Equality hiding (apply)
 import Unsafe.Coerce
 
@@ -39,17 +38,17 @@
 leibnizToRefl :: Leibniz a b -> a :=: b
 leibnizToRefl eq = apply eq Refl
 
-fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b
-fromLeibniz eq = apply eq (reflexivity sing)
+fromLeibniz :: (Preorder eq) => Leibniz a b -> eq a b
+fromLeibniz eq = apply eq (reflexivity Proxy)
 
-fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b
+fromRefl :: (Preorder eq) => a :=: b -> eq a b
 fromRefl Refl = reflexivity'
 
 reflToLeibniz :: a :=: b -> Leibniz a b
 reflToLeibniz Refl = Leibniz id
 
 class Preorder (eq :: k -> k -> *) where
-  reflexivity  :: Sing a -> eq a a
+  reflexivity  :: proxy a -> eq a a
   transitivity :: eq a b  -> eq b c -> eq a c
 
 class Preorder eq => Equality (eq :: k -> k -> *) where
@@ -85,12 +84,12 @@
 newtype Flip f a b = Flip { unFlip :: f b a }
 
 data Reason eq x y where
-  Because :: Sing y -> eq x y -> Reason eq x y
+  Because :: proxy y -> eq x y -> Reason eq x y
 
-reflexivity' :: (SingI x, Preorder r) => r x x
-reflexivity' = reflexivity sing
+reflexivity' :: (Preorder r) => r x x
+reflexivity' = reflexivity Proxy
 
-by, because :: Sing y -> eq x y -> Reason eq x y
+by, because :: proxy y -> eq x y -> Reason eq x y
 because = Because
 by      = Because
 
@@ -112,14 +111,14 @@
 (===) = (=<=)
 {-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
-(=~=) :: r x y -> Sing y -> r x y
+(=~=) :: r x y -> proxy y -> r x y
 eq =~= _ = eq
 
-start :: Preorder eq => Sing a -> eq a a
+start :: Preorder eq => proxy a -> eq a a
 start = reflexivity
 
-byDefinition :: (SingI a, Preorder eq) => eq a a
-byDefinition = reflexivity sing
+byDefinition :: (Preorder eq) => eq a a
+byDefinition = reflexivity Proxy
 
 admitted :: Reason eq x y
 admitted = undefined
@@ -128,7 +127,7 @@
 cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b
 cong Proxy Refl = Refl
 
-cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b
+cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b
 cong' _ Refl =  Refl
 
 -- | Type coercion. 'coerce' is using @unsafeCoerce a@.
diff --git a/Proof/Induction.hs b/Proof/Induction.hs
deleted file mode 100644
--- a/Proof/Induction.hs
+++ /dev/null
@@ -1,82 +0,0 @@
-{-# 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         (Sing)
-import Language.Haskell.TH     (Clause, Con (ForallC, InfixC, NormalC, RecC))
-import Language.Haskell.TH     (TypeQ, appT, appT, appsE, appsE, arrowT, arrowT)
-import Language.Haskell.TH     (clause, clause, conP, conP, cxt, cxt, forallT)
-import Language.Haskell.TH     (funD, funD, mkName, nameBase, newName)
-import Language.Haskell.TH     (normalB, normalB, promotedT, promotedT, reify)
-import Language.Haskell.TH     (sigD, sigD, varE, varE, varP, varP, varT, 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/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,9 +2,10 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.5.1.1
+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.
+                     Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.
 license:             BSD3
 license-file:        LICENSE
 author:              Hiromi ISHII
@@ -20,7 +21,7 @@
     location: git://github.com/konn/equational-reasoning-in-haskell.git
 
 library
-  exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction
+  exposed-modules:     Proof.Equational, Proof.Propositional
                      , Proof.Propositional.Inhabited
                      , Proof.Propositional.Empty
   other-modules:       Proof.Internal.THCompat
@@ -31,7 +32,6 @@
                      , template-haskell >= 2.11   && < 2.16
                      , th-extras        == 0.0.*
                      , void             >= 0.6    && < 0.8
-                     , singletons       >= 2.1    && < 2.6
   if impl(ghc >= 8.4)
      build-depends:    th-desugar       >= 1.6 && < 1.11
   else