diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -1,18 +1,18 @@
-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies          #-}
-{-# LANGUAGE TypeOperators, TypeSynonymInstances, KindSignatures            #-}
-module Proof.Equational (
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-                         (:~:)(..), (:=:)
-#else
-                         (:=:)(..), (:~:)
+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, KindSignatures #-}
+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables              #-}
+{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances, UndecidableInstances              #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-}
 #endif
+module Proof.Equational ( (:~:)(..), (:=:)
                         , sym, trans
                         , Equality(..), Preorder(..), reflexivity'
-                        ,(:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)
+                        , (:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)
                         , Reason(..), because, by, (===), start, byDefinition
                         , admitted, Proxy(..), cong, cong'
-                        , Proposition(..), (:~>), FromBool (..)
+                        , Proposition(..), HVec(..), FromBool (..)
+                        , applyNAry, applyNAry', fromBool'
                           -- * Conversion between equalities
                         , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl
                           -- * Coercion
@@ -22,10 +22,8 @@
                         ) where
 import Data.Proxy
 import Data.Singletons
-import Unsafe.Coerce
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
 import Data.Type.Equality hiding (apply)
-#endif
+import Unsafe.Coerce
 
 infix 4 :=:
 type a :\/: b = Either a b
@@ -34,39 +32,8 @@
 type a :/\: b = (a, b)
 infixr 3 :/\:
 
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
-data a :=: b where
-  Refl :: a :=: a
-type (:~:) = (:=:)
-infix 4 :~:
-trans :: a :=: b -> b :=: c -> a :=: c
-trans Refl Refl = Refl
-
-sym :: a :=: b -> b :=: a
-sym Refl = Refl
-
-deriving instance Eq   (a :=: b)
-deriving instance Show (a :=: b)
-deriving instance Ord  (a :=: b)
-
-instance a ~ b => Read (a :=: b) where
-  readsPrec d = readParen (d > 10) (\r -> [(Refl, s) | ("Refl",s) <- lex r ])
-
-instance a ~ b => Enum (a :=: b) where
-  toEnum 0 = Refl
-  toEnum _ = error "toEnum: bad argument"
-
-  fromEnum Refl = 0
-
-instance a ~ b => Bounded (a :=: b) where
-  minBound = Refl
-  maxBound = Refl
-
-#else
 type (:=:) = (:~:)
-#endif
 
-
 data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }
 
 leibnizToRefl :: Leibniz a b -> a :=: b
@@ -184,24 +151,60 @@
   coerce' xs = unsafeCoerce
   #-}
 
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
 class Proposition (f :: k -> *) where
-  type OriginalProp (f :: k -> *) (n :: k) :: *    
-#else
-class Proposition f where
-  type OriginalProp f n :: *
-#endif
+  type OriginalProp (f :: k -> *) (n :: k) :: *
   unWrap :: f n -> OriginalProp f n
   wrap   :: OriginalProp f n -> f n
 
-type family   (xs :: [*]) :~> (a :: *) :: *
-type instance '[]       :~> a = a
-type instance (x ': xs) :~> a = x -> (xs :~> a)
+data HVec (xs :: [*]) where
+  HNil :: HVec '[]
+  (:-) :: x -> HVec xs -> HVec (x ': xs)
 
+infixr 9 :-
+type family (xs :: [*]) :~> (a :: *) :: * where
+  '[]       :~> a = a
+  (x ': xs) :~> a = x -> (xs :~> a)
+
 infixr 1 :~>
 
+data HVecView (xs :: [*]) :: * where
+  HNilView  :: HVecView '[]
+  HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)
+
+deriving instance Show (HVecView xs)
+
+class KnownTypeList (xs :: [*]) where
+  viewHVec' :: HVecView xs
+
+instance KnownTypeList '[] where
+  viewHVec' = HNilView
+
+instance KnownTypeList ts => KnownTypeList (t ': ts) where
+  viewHVec' = HConsView Proxy viewHVec'
+
+viewHVec :: KnownTypeList ts => HVec ts -> HVecView ts
+viewHVec _ = viewHVec'
+
+newtype Magic (xs :: [*]) a = Magic { _viewHVec' :: KnownTypeList xs => a }
+
+withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a
+withKnownTypeList xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs
+
+apply' :: (KnownTypeList ts) => HVecView ts -> (HVec ts -> c) -> ts :~> c
+apply' HNilView f = f HNil
+apply' (HConsView Proxy ts) f = \a -> withKnownTypeList ts $
+  apply' ts (\ts' -> f $ a :- ts')
+
+applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
+applyNAry = apply' (viewHVec' :: HVecView ts)
+
+applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
+applyNAry' _ _ = applyNAry
+
 class FromBool (c :: *) where
   type Predicate c :: Bool
   type Args c :: [*]
-  fromBool :: Predicate c ~ True => Args c :~> c
+  fromBool :: Predicate c ~ 'True => HVec (Args c) -> c
+
+fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c , Predicate c ~ True) => proxy c -> Args c :~> c
+fromBool' pxyc = applyNAry' (Proxy :: Proxy (Args c)) pxyc fromBool
diff --git a/Proof/Induction.hs b/Proof/Induction.hs
--- a/Proof/Induction.hs
+++ b/Proof/Induction.hs
@@ -2,6 +2,8 @@
 {-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators              #-}
 {-# LANGUAGE UndecidableInstances, ViewPatterns                        #-}
 module Proof.Induction (genInduction) where
+import Proof.Internal.THCompat
+
 import Control.Applicative
 import Control.Monad
 import Data.Char
@@ -19,7 +21,7 @@
 genInduction :: Name -> String -> Q [Dec]
 genInduction typ fname0 = do
   let fname = mkName fname0
-  TyConI (normalizeDec -> DataD _ dName _ dCons _) <- reify typ
+  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
@@ -50,7 +52,7 @@
   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) : 
+           | 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) []
@@ -87,6 +89,6 @@
 getTyConName _             = Nothing
 
 normalizeDec :: Dec -> Dec
-normalizeDec d@(DataD _ _ _ _ _) = d
-normalizeDec (NewtypeD ctx name tvbs con names) = DataD ctx name tvbs [con] names
+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/Proof/Internal/THCompat.hs b/Proof/Internal/THCompat.hs
new file mode 100644
--- /dev/null
+++ b/Proof/Internal/THCompat.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE CPP, PatternSynonyms, TemplateHaskell, ViewPatterns #-}
+module Proof.Internal.THCompat where
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax
+import GHC.Exts (Constraint)
+
+mkDataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Dec
+mkDataD cxt name tvbndrs cons names =
+  DataD cxt name tvbndrs
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+        Nothing cons (map ConT names)
+#else
+        cons names
+#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 tvbndrs cons names <-
+  DataD cxt name tvbndrs
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+        _ cons (map typeName -> names)
+#else
+        cons names
+#endif
+
+pattern NewtypeDCompat cxt name tvbndrs con names <-
+  NewtypeD cxt name tvbndrs
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+        _ con (map typeName -> names)
+#else
+        con names
+#endif
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.7
+version:             0.3.0.0
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 description:         A simple convenient library to write equational / preorder proof as in Agda.
 license:             BSD3
@@ -12,9 +12,7 @@
 copyright:           (c) Hiromi ISHII 2013-2014
 category:            Math
 build-type:          Simple
-tested-with:         GHC == 7.6.3,
-                     GHC == 7.8.3, GHC == 7.8.4,
-                     GHC == 7.10.2
+tested-with:         GHC == 7.10.3, GHC == 8.0.1
 cabal-version:       >=1.8
 
 source-repository head
@@ -23,14 +21,11 @@
 
 library
   exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction
+  other-modules:       Proof.Internal.THCompat
   build-depends:       base             >= 4      && < 5
                ,       void             >= 0.6    && < 0.8
-               ,       template-haskell >= 2.8    && < 2.11
-  if impl(ghc < 7.8)
-    build-depends:     singletons       == 0.8.*
-                 ,     tagged           >= 0.6
+               ,       template-haskell
+  if impl(ghc < 7.10)
+    build-depends:     singletons       >= 0.8    && < 1.2
   else
-    if impl(ghc < 7.10)
-      build-depends:     singletons       >= 0.8    && < 1.2
-    else
-      build-depends:     singletons       == 2.0.*
+    build-depends:     singletons       >= 2.1    && < 2.3