diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,26 @@
+# Unreleased
+
+# 0.3.0.0
+
+## Main updates
+
+- Type/Kind level quasiquoter are added.
+- Evaluators are added to the top-level modules.
+- STLC and System F omega are tested with various examples.
+- Identifiers now accepts `_`.
+
+## Bug fixed
+
+- Substitutions are fixed with valid shifting.
+- STLC normalizer is fixed with valid beta-reduction.
+- Fix type inference for System F and System F omega.
+
+## Breaking changes
+
+- Names of quasiquoters are changed.
+- The order of arguments for substitution are changed.
+- Non-Ast modules now have explicit export lists.
+
 # 0.2.0.0
 
 ## Main updates
@@ -10,12 +33,12 @@
 
 ## Breaking changes
 
-- Move lifters and substitutions into dedicated modules.
-- Rename pretty printers.
-- Rename elaborators.
-- Rename quasiquoter.
-- Remove elaborated quasiquoter.
-- Change the type of elaborator and type checker.
+- Lifters and substitutions into dedicated modules are moved.
+- Pretty printers are renamed.
+- Elaborators are renamed.
+- Quasiquoter are renamed.
+- Elaborated quasiquoters are remove.
+- The types of elaborators and type checkers are changed.
 
 # 0.1.0.0
 
diff --git a/lambda-cube.cabal b/lambda-cube.cabal
--- a/lambda-cube.cabal
+++ b/lambda-cube.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           lambda-cube
-version:        0.2.0.0
+version:        0.3.0.0
 synopsis:       Haskell implementation of (some of) lambda cube calculi
 description:    Haskell implementation of the following 4 lambda calculi:
                 .
@@ -34,6 +34,7 @@
   exposed-modules:
       LambdaCube.Common.Parser
       LambdaCube.Common.PrettyPrinter
+      LambdaCube.Common.TH
       LambdaCube.STLC
       LambdaCube.STLC.Ast
       LambdaCube.STLC.Elaborator
@@ -137,8 +138,13 @@
 
 test-suite lambda-cube-test
   type: exitcode-stdio-1.0
-  main-is: Spec.hs
+  main-is: Test.hs
   other-modules:
+      LambdaCube.STLCTest
+      LambdaCube.STLCTestExample
+      LambdaCube.SystemFwTest
+      LambdaCube.SystemFwTestExample
+      LambdaCube.TestUtil
       Paths_lambda_cube
   hs-source-dirs:
       test
@@ -188,8 +194,10 @@
       TypeSynonymInstances
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-deriving-strategies -Wmissing-home-modules -Wmonomorphism-restriction -Wpartial-fields -Wredundant-constraints -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
   build-depends:
-      QuickCheck
-    , base
+      base
     , hspec
     , lambda-cube
+    , tasty
+    , tasty-hspec
+    , text
   default-language: Haskell2010
diff --git a/src/LambdaCube/Common/Parser.hs b/src/LambdaCube/Common/Parser.hs
--- a/src/LambdaCube/Common/Parser.hs
+++ b/src/LambdaCube/Common/Parser.hs
@@ -1,6 +1,27 @@
 {-# LANGUAGE OverloadedStrings #-}
-module LambdaCube.Common.Parser where
+module LambdaCube.Common.Parser
+  ( Parser
 
+  , topParser
+  , parenthesized
+  , identifier
+
+  , rightArrow
+  , atsignBackslash
+
+  , backslash
+  , atsign
+  , sharp
+  , colon
+  , dot
+  , openParenthesis
+  , closeParenthesis
+  , exclamationMark
+  , comma
+  , asterisk
+  , dollarsign
+  ) where
+
 import           Prelude              hiding (lex)
 
 import           Data.Text            (Text)
@@ -17,6 +38,9 @@
 parenthesized :: Parser a -> Parser a
 parenthesized = between openParenthesis closeParenthesis
 
+identifier :: Parser Text
+identifier = lex $ (Text.pack .) . (:) <$> letterChar <*> many (alphaNumChar <|> char '_')
+
 rightArrow, atsignBackslash :: Parser Text
 rightArrow = lex $ string "->"
 atsignBackslash = lex $ string "@\\"
@@ -33,9 +57,6 @@
 comma            = lex $ char ','
 asterisk         = lex $ char '*'
 dollarsign       = lex $ char '$'
-
-identifier :: Parser Text
-identifier = lex $ (Text.pack .) . (:) <$> letterChar <*> many alphaNumChar
 
 lex :: Parser a -> Parser a
 lex = (<* space)
diff --git a/src/LambdaCube/Common/PrettyPrinter.hs b/src/LambdaCube/Common/PrettyPrinter.hs
--- a/src/LambdaCube/Common/PrettyPrinter.hs
+++ b/src/LambdaCube/Common/PrettyPrinter.hs
@@ -1,18 +1,24 @@
 {-# LANGUAGE OverloadedStrings #-}
-module LambdaCube.Common.PrettyPrinter where
+module LambdaCube.Common.PrettyPrinter
+  ( wrapIfSpaced
+  , wrapIf
+  , wrap
 
+  , spaced
+  ) where
+
 import           Data.Text (Text)
 import qualified Data.Text as Text
 
 wrapIfSpaced :: Bool -> [Text] -> Text
 wrapIfSpaced b = wrapIf b . spaced
 
-wrap :: Text -> Text
-wrap t = "(" <> t <> ")"
-
 wrapIf :: Bool -> Text -> Text
 wrapIf True  = wrap
 wrapIf False = id
+
+wrap :: Text -> Text
+wrap t = "(" <> t <> ")"
 
 spaced :: [Text] -> Text
 spaced = Text.intercalate " "
diff --git a/src/LambdaCube/Common/TH.hs b/src/LambdaCube/Common/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/Common/TH.hs
@@ -0,0 +1,25 @@
+module LambdaCube.Common.TH
+  ( qExpBase
+
+  , converterBase
+  ) where
+
+import           Data.Data                  (Data)
+import           Data.Generics              (extQ)
+import           Data.Text                  (Text)
+import qualified Data.Text                  as Text
+import           LambdaCube.Common.Parser
+import           Language.Haskell.TH.Lib    (ExpQ)
+import           Language.Haskell.TH.Syntax (dataToExpQ, lift, loc_start,
+                                             location)
+import qualified Text.Megaparsec            as P
+
+qExpBase :: Data a => Parser a -> (forall b. Data b => b -> Maybe ExpQ) -> String -> ExpQ
+qExpBase p conv str = do
+  l <- location
+  case P.parse p ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
+    Right e  -> dataToExpQ conv e
+    Left err -> fail $ P.errorBundlePretty err
+
+converterBase :: Data b => b -> Maybe ExpQ
+converterBase = const Nothing `extQ` (Just . lift :: Text -> Maybe ExpQ)
diff --git a/src/LambdaCube/STLC.hs b/src/LambdaCube/STLC.hs
--- a/src/LambdaCube/STLC.hs
+++ b/src/LambdaCube/STLC.hs
@@ -1,6 +1,7 @@
 module LambdaCube.STLC
   ( module LambdaCube.STLC.Ast
   , module LambdaCube.STLC.Elaborator
+  , module LambdaCube.STLC.Evaluator
   , module LambdaCube.STLC.Lifter
   , module LambdaCube.STLC.Normalizer
   , module LambdaCube.STLC.Parser
@@ -13,6 +14,7 @@
 import LambdaCube.STLC.Ast
 
 import LambdaCube.STLC.Elaborator
+import LambdaCube.STLC.Evaluator
 import LambdaCube.STLC.Lifter
 import LambdaCube.STLC.Normalizer
 import LambdaCube.STLC.Parser
diff --git a/src/LambdaCube/STLC/Ast.hs b/src/LambdaCube/STLC/Ast.hs
--- a/src/LambdaCube/STLC/Ast.hs
+++ b/src/LambdaCube/STLC/Ast.hs
@@ -4,13 +4,6 @@
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
-data ExtLCType
-  = ExtLCBase
-  | ExtLCArr ExtLCType ExtLCType
-  | ExtLCMTVar String
-  deriving stock (Eq, Show, Data, Lift)
-infixr 5 `ExtLCArr`
-
 data ExtLCTerm
   = ExtLCVar Text
   | ExtLCLam Text ExtLCType ExtLCTerm
@@ -19,11 +12,12 @@
   deriving stock (Eq, Show, Data, Lift)
 infixl 6 `ExtLCApp`
 
-data LCType
-  = LCBase
-  | LCArr LCType LCType
+data ExtLCType
+  = ExtLCBase
+  | ExtLCArr ExtLCType ExtLCType
+  | ExtLCMTVar String
   deriving stock (Eq, Show, Data, Lift)
-infixr 5 `LCArr`
+infixr 5 `ExtLCArr`
 
 data LCTerm
   = LCVar Int
@@ -31,6 +25,12 @@
   | LCApp LCTerm LCTerm
   deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCApp`
+
+data LCType
+  = LCBase
+  | LCArr LCType LCType
+  deriving stock (Eq, Show, Data, Lift)
+infixr 5 `LCArr`
 
 data LCValue
   = LCValLam LCType LCTerm
diff --git a/src/LambdaCube/STLC/Elaborator.hs b/src/LambdaCube/STLC/Elaborator.hs
--- a/src/LambdaCube/STLC/Elaborator.hs
+++ b/src/LambdaCube/STLC/Elaborator.hs
@@ -1,24 +1,27 @@
-module LambdaCube.STLC.Elaborator where
+module LambdaCube.STLC.Elaborator
+  ( elaborate
+  , elaborateType
+  ) where
 
 import           Data.List           (elemIndex)
 import qualified Data.Text           as Text
 import           LambdaCube.STLC.Ast
 
-elaborateType :: ExtLCType -> LCType
-elaborateType = go
-  where
-    go ExtLCBase = LCBase
-    go (ExtLCArr a b) = go a `LCArr` go b
-    go (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
-
 elaborate :: ExtLCTerm -> LCTerm
 elaborate = go []
   where
-    go l (ExtLCVar v)
-      | Just idx <- v `elemIndex` l
+    go l (ExtLCVar x)
+      | Just idx <- x `elemIndex` l
       = LCVar idx
       | otherwise
-      = error $ "Variable " <> Text.unpack v <> " is not in scope"
-    go l (ExtLCLam v t b) = LCLam (elaborateType t) $ go (v : l) b
+      = error $ "Variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCLam x t b) = LCLam (elaborateType t) $ go (x : l) b
     go l (ExtLCApp f a) = go l f `LCApp` go l a
     go _ (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
+
+elaborateType :: ExtLCType -> LCType
+elaborateType = go
+  where
+    go ExtLCBase = LCBase
+    go (ExtLCArr a b) = go a `LCArr` go b
+    go (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
diff --git a/src/LambdaCube/STLC/Evaluator.hs b/src/LambdaCube/STLC/Evaluator.hs
--- a/src/LambdaCube/STLC/Evaluator.hs
+++ b/src/LambdaCube/STLC/Evaluator.hs
@@ -1,4 +1,6 @@
-module LambdaCube.STLC.Evaluator where
+module LambdaCube.STLC.Evaluator
+  ( evaluate
+  ) where
 
 import           LambdaCube.STLC.Ast
 import           LambdaCube.STLC.Substitution
@@ -11,4 +13,4 @@
     go (LCApp f a)
       | LCValLam _ b <- go f
       , v <- go a
-      = go $ substituteValue 0 v b
+      = go $ substituteValue v 0 b
diff --git a/src/LambdaCube/STLC/Lifter.hs b/src/LambdaCube/STLC/Lifter.hs
--- a/src/LambdaCube/STLC/Lifter.hs
+++ b/src/LambdaCube/STLC/Lifter.hs
@@ -1,4 +1,7 @@
-module LambdaCube.STLC.Lifter where
+module LambdaCube.STLC.Lifter
+  ( liftLCValue
+  , liftLCNormal
+  ) where
 
 import           LambdaCube.STLC.Ast
 
@@ -10,5 +13,5 @@
 liftLCNormal (LCNormNeut nt) = liftLCNeutral nt
 
 liftLCNeutral :: LCNeutralTerm -> LCTerm
-liftLCNeutral (LCNeutVar n) = LCVar n
+liftLCNeutral (LCNeutVar x) = LCVar x
 liftLCNeutral (LCNeutApp f a) = liftLCNeutral f `LCApp` liftLCNormal a
diff --git a/src/LambdaCube/STLC/Normalizer.hs b/src/LambdaCube/STLC/Normalizer.hs
--- a/src/LambdaCube/STLC/Normalizer.hs
+++ b/src/LambdaCube/STLC/Normalizer.hs
@@ -1,4 +1,6 @@
-module LambdaCube.STLC.Normalizer where
+module LambdaCube.STLC.Normalizer
+  ( normalize
+  ) where
 
 import           LambdaCube.STLC.Ast
 import           LambdaCube.STLC.Substitution
@@ -6,11 +8,11 @@
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
   where
-    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCVar x) = LCNormNeut $ LCNeutVar x
     go (LCLam t b) = LCNormLam t $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam t b   -> LCNormLam t $ substituteNormalInNormal 0 a' b
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+        LCNormLam _ b -> substituteNormalInNormal a' 0 b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
       where
         a' = go a
diff --git a/src/LambdaCube/STLC/Parser.hs b/src/LambdaCube/STLC/Parser.hs
--- a/src/LambdaCube/STLC/Parser.hs
+++ b/src/LambdaCube/STLC/Parser.hs
@@ -1,4 +1,7 @@
-module LambdaCube.STLC.Parser where
+module LambdaCube.STLC.Parser
+  ( pTopTerm
+  , pTopType
+  ) where
 
 import           Data.Foldable            (Foldable (foldl'))
 import           Data.Functor             (($>))
@@ -7,30 +10,33 @@
 import           LambdaCube.STLC.Ast
 import           Text.Megaparsec
 
-pTopLC :: Parser ExtLCTerm
-pTopLC = topParser pLC
+pTopTerm :: Parser ExtLCTerm
+pTopTerm = topParser pTerm
 
-pLC :: Parser ExtLCTerm
-pLC = pLam<|> pApp
+pTerm :: Parser ExtLCTerm
+pTerm = pLam <|> pApp
 
 pLam :: Parser ExtLCTerm
 pLam =
   ExtLCLam
   <$> (backslash *> identifier)
   <*> (colon *> pType)
-  <*> (dot *> pLC)
+  <*> (dot *> pTerm)
 
 pApp :: Parser ExtLCTerm
 pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = pVar <|> pMVar <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pTerm
 
 pVar :: Parser ExtLCTerm
 pVar = ExtLCVar <$> identifier
 
 pMVar :: Parser ExtLCTerm
 pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
+
+pTopType :: Parser ExtLCType
+pTopType = topParser pType
 
 pType :: Parser ExtLCType
 pType = foldr1 ExtLCArr <$> sepBy1 pAType rightArrow
diff --git a/src/LambdaCube/STLC/PrettyPrinter.hs b/src/LambdaCube/STLC/PrettyPrinter.hs
--- a/src/LambdaCube/STLC/PrettyPrinter.hs
+++ b/src/LambdaCube/STLC/PrettyPrinter.hs
@@ -2,30 +2,41 @@
   TODO: Use real pretty printer library
 -}
 {-# LANGUAGE OverloadedStrings #-}
-module LambdaCube.STLC.PrettyPrinter where
+module LambdaCube.STLC.PrettyPrinter
+  ( prettyUnnamedTerm
+  , prettyShowUnnamedTerm
+  , prettyUnnamedType
+  , prettyShowUnnamedType
+  ) where
 
 import           Data.Text                       (Text)
 import qualified Data.Text                       as Text
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.STLC.Ast
 
-prettyUnnamedType :: LCType -> Text
-prettyUnnamedType = prettyUnnamedTypePrec 0
-
 prettyUnnamedTerm :: LCTerm -> Text
 prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
-prettyUnnamedTypePrec :: Int -> LCType -> Text
-prettyUnnamedTypePrec = go
-  where
-    go _ LCBase      = "#"
-    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+prettyShowUnnamedTerm :: LCTerm -> String
+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm
 
+prettyUnnamedType :: LCType -> Text
+prettyUnnamedType = prettyUnnamedTypePrec 0
+
+prettyShowUnnamedType :: LCType -> String
+prettyShowUnnamedType = Text.unpack . prettyUnnamedType
+
 prettyUnnamedTermPrec :: Int -> LCTerm -> Text
 prettyUnnamedTermPrec = go
   where
     pTP = prettyUnnamedTypePrec
 
-    go _ (LCVar n)   = Text.pack $ show n
+    go _ (LCVar x)   = Text.pack $ show x
     go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
     go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+
+prettyUnnamedTypePrec :: Int -> LCType -> Text
+prettyUnnamedTypePrec = go
+  where
+    go _ LCBase      = "#"
+    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
diff --git a/src/LambdaCube/STLC/Substitution.hs b/src/LambdaCube/STLC/Substitution.hs
--- a/src/LambdaCube/STLC/Substitution.hs
+++ b/src/LambdaCube/STLC/Substitution.hs
@@ -1,28 +1,70 @@
-module LambdaCube.STLC.Substitution where
+{-# LANGUAGE ViewPatterns #-}
+module LambdaCube.STLC.Substitution
+  ( substituteValue
+  , substituteNormalInNormal
+  ) where
 
 import           LambdaCube.STLC.Ast
 import           LambdaCube.STLC.Lifter
 
-substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
-substituteValue n v = go n
+substituteValue :: LCValue -> Int -> LCTerm -> LCTerm
+substituteValue v = substDefValue (v, 0)
+
+substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal v = substDefNormalInNormal (v, 0)
+
+substDefValue :: (LCValue, Int) -> Int -> LCTerm -> LCTerm
+substDefValue = go
   where
-    go m e@(LCVar l) = if m == l then liftLCValue v else e
-    go m (LCLam t b) = LCLam t $ go (m + 1) b
-    go m (LCApp f a) = go m f `LCApp` go m a
+    go dv     x (LCVar ((== x) -> True))  = shiftValue dv
+    go _      x e@(LCVar ((< x) -> True)) = e
+    go _      _ (LCVar y)                 = LCVar $ y - 1
+    go (v, s) x (LCLam t b)               = LCLam t $ go (v, s + 1) (x + 1) b
+    go dv     x (LCApp f a)               = go dv x f `LCApp` go dv x a
 
-substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormalInNormal n nv = go n
+substDefNormalInNormal :: (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm
+substDefNormalInNormal = go
   where
-    go m (LCNormLam t b)   = LCNormLam t $ go (m + 1) b
-    go m (LCNormNeut neut) = substituteNormalInNeutral m nv neut
+    go (v, s) x (LCNormLam t b) = LCNormLam t $ go (v, s + 1) (x + 1) b
+    go dv     x (LCNormNeut nt) = substDefNormalInNeutral dv x nt
 
-substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNormalInNeutral n nv = go n
+substDefNormalInNeutral :: (LCNormalTerm, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
+substDefNormalInNeutral dv x = go
   where
-    go m e@(LCNeutVar l) = if m == l then nv else LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv
+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e
+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1
+    go (LCNeutApp f a) =
+      case go f of
+        LCNormLam _ b -> substituteNormalInNormal a' 0 b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
       where
-        a' = substituteNormalInNormal m nv a
+        a' = substDefNormalInNormal dv x a
+
+shift :: (LCTerm, Int) -> LCTerm
+shift = shiftMin 0
+
+shiftMin :: Int -> (LCTerm, Int) -> LCTerm
+shiftMin n' (v, s) = go n' v
+  where
+    go n (LCVar x)   = LCVar $ if x < n then x else x + s
+    go n (LCLam t b) = LCLam t $ go (n + 1) b
+    go n (LCApp f a) = go n f `LCApp` go n a
+
+shiftValue :: (LCValue, Int) -> LCTerm
+shiftValue (v, s) = shift (liftLCValue v, s)
+
+shiftNormal :: (LCNormalTerm, Int) -> LCNormalTerm
+shiftNormal = shiftNormalMin 0
+
+shiftNormalMin :: Int -> (LCNormalTerm, Int) -> LCNormalTerm
+shiftNormalMin n' (v, s) = go n' v
+  where
+    go n (LCNormLam t b) = LCNormLam t $ go (n + 1) b
+    go n (LCNormNeut nt) = LCNormNeut $ shiftNeutralMin n (nt, s)
+
+shiftNeutralMin :: Int -> (LCNeutralTerm, Int) -> LCNeutralTerm
+shiftNeutralMin n (v, s) = go v
+  where
+    go (LCNeutVar x)   = LCNeutVar $ if x < n then x else x + s
+    go (LCNeutApp f a) = go f `LCNeutApp` shiftNormalMin n (a, s)
diff --git a/src/LambdaCube/STLC/TH.hs b/src/LambdaCube/STLC/TH.hs
--- a/src/LambdaCube/STLC/TH.hs
+++ b/src/LambdaCube/STLC/TH.hs
@@ -1,45 +1,57 @@
 module LambdaCube.STLC.TH
-  ( lc
+  ( qTerm
+  , qType
   ) where
 
 import           Data.Data                  (Data)
 import           Data.Generics              (extQ)
-import           Data.Text                  (Text)
-import qualified Data.Text                  as Text
+import           LambdaCube.Common.TH
 import           LambdaCube.STLC.Ast
 import           LambdaCube.STLC.Parser
 import           Language.Haskell.TH.Lib    (ExpQ, varE)
 import           Language.Haskell.TH.Quote  (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,
-                                             location, mkName)
-import qualified Text.Megaparsec            as P
-import qualified Text.Megaparsec.Error      as PE
+import           Language.Haskell.TH.Syntax (mkName)
 
-lc :: QuasiQuoter
-lc =
+qTerm :: QuasiQuoter
+qTerm =
   QuasiQuoter
-    { quoteExp = expLc
+    { quoteExp = qExpTerm
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-expLc :: String -> ExpQ
-expLc str = do
-  l <- location
-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> dataToExpQ converter e
-    Left err -> fail $ PE.errorBundlePretty err
+qExpTerm :: String -> ExpQ
+qExpTerm = qExpBase pTopTerm converter
   where
     converter :: Data b => b -> Maybe ExpQ
     converter =
-      const Nothing
+      converterBase
       `extQ` quotedMVar
       `extQ` quotedMTVar
-      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
     quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
     quotedMVar _             = Nothing
+
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
+
+qType :: QuasiQuoter
+qType =
+  QuasiQuoter
+    { quoteExp = qExpType
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+qExpType :: String -> ExpQ
+qExpType = qExpBase pTopType converter
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      converterBase
+      `extQ` quotedMTVar
 
     quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
     quotedMTVar _              = Nothing
diff --git a/src/LambdaCube/STLC/TypeChecker.hs b/src/LambdaCube/STLC/TypeChecker.hs
--- a/src/LambdaCube/STLC/TypeChecker.hs
+++ b/src/LambdaCube/STLC/TypeChecker.hs
@@ -1,4 +1,6 @@
-module LambdaCube.STLC.TypeChecker where
+module LambdaCube.STLC.TypeChecker
+  ( infer
+  ) where
 
 import           Data.List           (uncons)
 import           LambdaCube.STLC.Ast
@@ -6,7 +8,7 @@
 infer :: LCTerm -> LCType
 infer = go []
   where
-    go l (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n l
+    go l (LCVar x) = maybe (error "Out-of-scope variable") fst . uncons $ drop x l
     go l (LCLam t b) = t `LCArr` go (t : l) b
     go l (LCApp f a)
       | LCArr at rt <- go l f
diff --git a/src/LambdaCube/SystemF.hs b/src/LambdaCube/SystemF.hs
--- a/src/LambdaCube/SystemF.hs
+++ b/src/LambdaCube/SystemF.hs
@@ -1,6 +1,7 @@
 module LambdaCube.SystemF
   ( module LambdaCube.SystemF.Ast
   , module LambdaCube.SystemF.Elaborator
+  , module LambdaCube.SystemF.Evaluator
   , module LambdaCube.SystemF.Lifter
   , module LambdaCube.SystemF.Normalizer
   , module LambdaCube.SystemF.Parser
@@ -13,6 +14,7 @@
 import LambdaCube.SystemF.Ast
 
 import LambdaCube.SystemF.Elaborator
+import LambdaCube.SystemF.Evaluator
 import LambdaCube.SystemF.Lifter
 import LambdaCube.SystemF.Normalizer
 import LambdaCube.SystemF.Parser
diff --git a/src/LambdaCube/SystemF/Ast.hs b/src/LambdaCube/SystemF/Ast.hs
--- a/src/LambdaCube/SystemF/Ast.hs
+++ b/src/LambdaCube/SystemF/Ast.hs
@@ -4,15 +4,6 @@
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
-data ExtLCType
-  = ExtLCBase
-  | ExtLCTVar Text
-  | ExtLCArr ExtLCType ExtLCType
-  | ExtLCUniv Text ExtLCType
-  | ExtLCMTVar String
-  deriving stock (Eq, Show, Data, Lift)
-infixr 5 `ExtLCArr`
-
 data ExtLCTerm
   = ExtLCVar Text
   | ExtLCLam Text ExtLCType ExtLCTerm
@@ -24,13 +15,14 @@
 infixl 6 `ExtLCApp`
 infixl 6 `ExtLCTApp`
 
-data LCType
-  = LCBase
-  | LCTVar Int
-  | LCArr LCType LCType
-  | LCUniv LCType
+data ExtLCType
+  = ExtLCBase
+  | ExtLCTVar Text
+  | ExtLCArr ExtLCType ExtLCType
+  | ExtLCUniv Text ExtLCType
+  | ExtLCMTVar String
   deriving stock (Eq, Show, Data, Lift)
-infixr 5 `LCArr`
+infixr 5 `ExtLCArr`
 
 data LCTerm
   = LCVar Int
@@ -41,6 +33,14 @@
   deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCApp`
 infixl 6 `LCTApp`
+
+data LCType
+  = LCBase
+  | LCTVar Int
+  | LCArr LCType LCType
+  | LCUniv LCType
+  deriving stock (Eq, Show, Data, Lift)
+infixr 5 `LCArr`
 
 data LCValue
   = LCValLam LCType LCTerm
diff --git a/src/LambdaCube/SystemF/Elaborator.hs b/src/LambdaCube/SystemF/Elaborator.hs
--- a/src/LambdaCube/SystemF/Elaborator.hs
+++ b/src/LambdaCube/SystemF/Elaborator.hs
@@ -1,4 +1,7 @@
-module LambdaCube.SystemF.Elaborator where
+module LambdaCube.SystemF.Elaborator
+  ( elaborate
+  , elaborateType
+  ) where
 
 import           Data.List              (elemIndex)
 import           Data.Text              (Text)
@@ -15,7 +18,7 @@
       = error $ "Term variable " <> Text.unpack x <> " is not in scope"
     go tl vl (ExtLCLam x t b) = LCLam (elaborateType tl t) $ go tl (x : vl) b
     go tl vl (ExtLCApp f a) = go tl vl f `LCApp` go tl vl a
-    go tl vl (ExtLCTLam x b) = LCTLam $ go (x : tl) vl b
+    go tl vl (ExtLCTLam p b) = LCTLam $ go (p : tl) vl b
     go tl vl (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t
     go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
 
@@ -23,11 +26,11 @@
 elaborateType = go
   where
     go _ ExtLCBase = LCBase
-    go l (ExtLCTVar x)
-      | Just n <- x `elemIndex` l
+    go l (ExtLCTVar p)
+      | Just n <- p `elemIndex` l
       = LCTVar n
       | otherwise
-      = error $ "Type variable " <> Text.unpack x <> " is not in scope"
+      = error $ "Type variable " <> Text.unpack p <> " is not in scope"
     go l (ExtLCArr a b) = go l a `LCArr` go l b
-    go l (ExtLCUniv x a) = LCUniv $ go (x : l) a
+    go l (ExtLCUniv p a) = LCUniv $ go (p : l) a
     go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
diff --git a/src/LambdaCube/SystemF/Evaluator.hs b/src/LambdaCube/SystemF/Evaluator.hs
--- a/src/LambdaCube/SystemF/Evaluator.hs
+++ b/src/LambdaCube/SystemF/Evaluator.hs
@@ -1,4 +1,6 @@
-module LambdaCube.SystemF.Evaluator where
+module LambdaCube.SystemF.Evaluator
+  ( evaluate
+  ) where
 
 import           LambdaCube.SystemF.Ast
 import           LambdaCube.SystemF.Substitution
@@ -11,12 +13,12 @@
     go (LCApp f a)
       | LCValLam _ b <- go f
       , v <- go a
-      = go $ substituteValue 0 v b
+      = go $ substituteValue v 0 b
       | otherwise
       = error "Did you really type check this?"
     go (LCTLam b) = LCValTLam b
     go (LCTApp f t)
       | LCValTLam b <- go f
-      = go $ substituteType 0 t b
+      = go $ substituteType t 0 b
       | otherwise
       = error "Did you really type check this?"
diff --git a/src/LambdaCube/SystemF/Lifter.hs b/src/LambdaCube/SystemF/Lifter.hs
--- a/src/LambdaCube/SystemF/Lifter.hs
+++ b/src/LambdaCube/SystemF/Lifter.hs
@@ -1,4 +1,7 @@
-module LambdaCube.SystemF.Lifter where
+module LambdaCube.SystemF.Lifter
+  ( liftLCValue
+  , liftLCNormal
+  ) where
 
 import           LambdaCube.SystemF.Ast
 
@@ -12,6 +15,6 @@
 liftLCNormal (LCNormNeut nt) = liftLCNeutral nt
 
 liftLCNeutral :: LCNeutralTerm -> LCTerm
-liftLCNeutral (LCNeutVar n)    = LCVar n
+liftLCNeutral (LCNeutVar x)    = LCVar x
 liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a
 liftLCNeutral (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
diff --git a/src/LambdaCube/SystemF/Normalizer.hs b/src/LambdaCube/SystemF/Normalizer.hs
--- a/src/LambdaCube/SystemF/Normalizer.hs
+++ b/src/LambdaCube/SystemF/Normalizer.hs
@@ -6,18 +6,18 @@
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
   where
-    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCVar x) = LCNormNeut $ LCNeutVar x
     go (LCLam t b) = LCNormLam t $ go b
     go (LCTLam b) = LCNormTLam $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
-        LCNormTLam _    -> error "Did you really type check this?"
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+        LCNormLam _ b -> substituteNormalInNormal a' 0 b
+        LCNormTLam _  -> error "Did you really type check this?"
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
       where
         a' = go a
     go (LCTApp f t) =
       case go f of
-        LCNormLam _ _   -> error "Did you really type check this?"
-        LCNormTLam b    -> substituteTypeInNormal 0 t b
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
+        LCNormLam _ _ -> error "Did you really type check this?"
+        LCNormTLam b  -> substituteTypeInNormal t 0 b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t
diff --git a/src/LambdaCube/SystemF/Parser.hs b/src/LambdaCube/SystemF/Parser.hs
--- a/src/LambdaCube/SystemF/Parser.hs
+++ b/src/LambdaCube/SystemF/Parser.hs
@@ -1,4 +1,7 @@
-module LambdaCube.SystemF.Parser where
+module LambdaCube.SystemF.Parser
+  ( pTopTerm
+  , pTopType
+  ) where
 
 import           Data.Foldable            (Foldable (foldl'))
 import           Data.Function            ((&))
@@ -9,24 +12,24 @@
 import           Text.Megaparsec
 import qualified Data.Text as Text
 
-pTopLC :: Parser ExtLCTerm
-pTopLC = topParser pLC
+pTopTerm :: Parser ExtLCTerm
+pTopTerm = topParser pTerm
 
-pLC :: Parser ExtLCTerm
-pLC = pTLam <|> pLam <|> pApp
+pTerm :: Parser ExtLCTerm
+pTerm = pTLam <|> pLam <|> pApp
 
 pTLam :: Parser ExtLCTerm
 pTLam =
   ExtLCTLam
   <$> (atsignBackslash *> identifier <* colon <* asterisk)
-  <*> (dot *> pLC)
+  <*> (dot *> pTerm)
 
 pLam :: Parser ExtLCTerm
 pLam =
   ExtLCLam
   <$> (backslash *> identifier)
   <*> (colon *> pType)
-  <*> (dot *> pLC)
+  <*> (dot *> pTerm)
 
 pApp :: Parser ExtLCTerm
 pApp = foldl' (&) <$> pATerm <*> many pAppArg
@@ -39,13 +42,16 @@
     else flip ExtLCApp <$> pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = pVar <|> pMVar <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pTerm
 
 pVar :: Parser ExtLCTerm
 pVar = ExtLCVar <$> identifier
 
 pMVar :: Parser ExtLCTerm
 pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
+
+pTopType :: Parser ExtLCType
+pTopType = topParser pType
 
 pType :: Parser ExtLCType
 pType = pUniv <|> pArr
diff --git a/src/LambdaCube/SystemF/PrettyPrinter.hs b/src/LambdaCube/SystemF/PrettyPrinter.hs
--- a/src/LambdaCube/SystemF/PrettyPrinter.hs
+++ b/src/LambdaCube/SystemF/PrettyPrinter.hs
@@ -2,34 +2,45 @@
   TODO: Use real pretty printer library
 -}
 {-# LANGUAGE OverloadedStrings #-}
-module LambdaCube.SystemF.PrettyPrinter where
+module LambdaCube.SystemF.PrettyPrinter
+  ( prettyUnnamedTerm
+  , prettyShowUnnamedTerm
+  , prettyUnnamedType
+  , prettyShowUnnamedType
+  ) where
 
 import           Data.Text                       (Text)
 import qualified Data.Text                       as Text
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.SystemF.Ast
 
-prettyUnnamedType :: LCType -> Text
-prettyUnnamedType = prettyUnnamedTypePrec 0
-
 prettyUnnamedTerm :: LCTerm -> Text
 prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
-prettyUnnamedTypePrec :: Int -> LCType -> Text
-prettyUnnamedTypePrec = go
-  where
-    go _ LCBase      = "#"
-    go _ (LCTVar i)  = Text.pack $ show i
-    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
-    go p (LCUniv b)  = wrapIfSpaced (p > 0) ["! : * ,", go 0 b]
+prettyShowUnnamedTerm :: LCTerm -> String
+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm
 
+prettyUnnamedType :: LCType -> Text
+prettyUnnamedType = prettyUnnamedTypePrec 0
+
+prettyShowUnnamedType :: LCType -> String
+prettyShowUnnamedType = Text.unpack . prettyUnnamedType
+
 prettyUnnamedTermPrec :: Int -> LCTerm -> Text
 prettyUnnamedTermPrec = go
   where
     pTP = prettyUnnamedTypePrec
 
-    go _ (LCVar i)    = Text.pack $ show i
+    go _ (LCVar x)    = Text.pack $ show x
     go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
     go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
     go p (LCTLam b)   = wrapIfSpaced (p > 0) ["@\\ : * .", go 0 b]
     go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]
+
+prettyUnnamedTypePrec :: Int -> LCType -> Text
+prettyUnnamedTypePrec = go
+  where
+    go _ LCBase      = "#"
+    go _ (LCTVar p)  = Text.pack $ show p
+    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+    go p (LCUniv b)  = wrapIfSpaced (p > 0) ["! : * ,", go 0 b]
diff --git a/src/LambdaCube/SystemF/Substitution.hs b/src/LambdaCube/SystemF/Substitution.hs
--- a/src/LambdaCube/SystemF/Substitution.hs
+++ b/src/LambdaCube/SystemF/Substitution.hs
@@ -1,82 +1,153 @@
-module LambdaCube.SystemF.Substitution where
+{-# LANGUAGE ViewPatterns #-}
+module LambdaCube.SystemF.Substitution
+  ( substituteType
+  , substituteTypeInType
+  , substituteValue
+  , substituteNormalInNormal
+  , substituteTypeInNormal
 
+  , shiftType
+  ) where
+
 import           LambdaCube.SystemF.Ast
 import           LambdaCube.SystemF.Lifter
 
-substituteType :: Int -> LCType -> LCTerm -> LCTerm
-substituteType n v = go n
+substituteType :: LCType -> Int -> LCTerm -> LCTerm
+substituteType v = substDefType (v, 0)
+
+substituteTypeInType :: LCType -> Int -> LCType -> LCType
+substituteTypeInType v = substDefTypeInType (v, 0)
+
+substituteValue :: LCValue -> Int -> LCTerm -> LCTerm
+substituteValue v = substDefValue (v, 0, 0)
+
+substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal v = substDefNormalInNormal (v, 0, 0)
+
+substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm
+substituteTypeInNormal v = substDefTypeInNormal (v, 0)
+
+substDefType :: (LCType, Int) -> Int -> LCTerm -> LCTerm
+substDefType = go
   where
-    go _ e@(LCVar _)  = e
-    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam b)   = LCTLam $ go (m + 1) b
-    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
+    go _      _ e@(LCVar _)  = e
+    go dv     p (LCLam t b)  = LCLam (substDefTypeInType dv p t) $ go dv p b
+    go dv     p (LCApp f a)  = go dv p f `LCApp` go dv p a
+    go (v, r) p (LCTLam b)   = LCTLam $ go (v, r + 1) (p + 1) b
+    go dv     p (LCTApp f t) = go dv p f `LCTApp` substDefTypeInType dv p t
 
-substituteTypeInType :: Int -> LCType -> LCType -> LCType
-substituteTypeInType n v = go n
+substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType
+substDefTypeInType = go
   where
-    go _ LCBase       = LCBase
-    go m e@(LCTVar l) = if m == l then v else e
-    go m (LCArr a b)  = go m a `LCArr` go m b
-    go m (LCUniv a)   = LCUniv $ go (m + 1) a
+    go _      _ LCBase                     = LCBase
+    go dv     p (LCTVar ((== p) -> True))  = shiftType dv
+    go _      p e@(LCTVar ((< p) -> True)) = e
+    go _      _ (LCTVar q)                 = LCTVar $ q - 1
+    go dv     p (LCArr a b)                = go dv p a `LCArr` go dv p b
+    go (v, r) p (LCUniv a)                 = LCUniv $ go (v, r + 1) (p + 1) a
 
-substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
-substituteValue n v = go n
+substDefValue :: (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm
+substDefValue = go
   where
-    go m e@(LCVar l)  = if m == l then liftLCValue v else e
-    go m (LCLam t b)  = LCLam t $ go (m + 1) b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam b)   = LCTLam $ go m b
-    go m (LCTApp f t) = go m f `LCTApp` t
+    go dv        x (LCVar ((== x) -> True))  = shiftValue dv
+    go _         x e@(LCVar ((< x) -> True)) = e
+    go _         _ (LCVar y)                 = LCVar $ y - 1
+    go (v, r, s) x (LCLam t b)               = LCLam t $ go (v, r, s + 1) (x + 1) b
+    go dv        x (LCApp f a)               = go dv x f `LCApp` go dv x a
+    go (v, r, s) x (LCTLam b)                = LCTLam $ go (v, r + 1, s) x b
+    go dv        x (LCTApp f t)              = go dv x f `LCTApp` t
 
-substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormalInNormal n v = go n
+substDefNormalInNormal :: (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm
+substDefNormalInNormal = go
   where
-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
-    go m (LCNormTLam b)  = LCNormTLam $ go m b
-    go m (LCNormNeut nt) = substituteNormalInNeutral m v nt
+    go (v, r, s) x (LCNormLam t b) = LCNormLam t $ go (v, r, s + 1) (x + 1) b
+    go (v, r, s) x (LCNormTLam b)  = LCNormTLam $ go (v, r + 1, s) x b
+    go dv        x (LCNormNeut nt) = substDefNormalInNeutral dv x nt
 
-substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNormalInNeutral n v = go n
+substDefNormalInNeutral :: (LCNormalTerm, Int, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
+substDefNormalInNeutral dv x = go
   where
-    go m e@(LCNeutVar l)
-      | m == l = v
-      | otherwise = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b -> substituteNormalInNormal 0 a' b
+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv
+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e
+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1
+    go (LCNeutApp f a) =
+      case go f of
+        LCNormLam _ b -> substituteNormalInNormal a' 0 b
         LCNormTLam _  -> error "Did you really type check this?"
         LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
       where
-        a' = substituteNormalInNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
+        a' = substDefNormalInNormal dv x a
+    go (LCNeutTApp f t) =
+      case go f of
         LCNormLam _ _ -> error "Did you really type check this?"
-        LCNormTLam b  -> substituteTypeInNormal 0 t b
+        LCNormTLam b  -> substituteTypeInNormal t 0 b
         LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t
 
-substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
-substituteTypeInNormal n v = go n
+substDefTypeInNormal :: (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm
+substDefTypeInNormal = go
   where
-    go m (LCNormLam t b) = LCNormLam (substituteTypeInType m v t) $ go m b
-    go m (LCNormTLam b)  = LCNormTLam $ go (m + 1) b
-    go m (LCNormNeut nt) = substituteTypeInNeutral m v nt
+    go dv     p (LCNormLam t b) = LCNormLam (substDefTypeInType dv p t) $ go dv p b
+    go (v, r) p (LCNormTLam b)  = LCNormTLam $ go (v, r + 1) (p + 1) b
+    go dv     p (LCNormNeut nt) = substDefTypeInNeutral dv p nt
 
-substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
-substituteTypeInNeutral n v = go n
+substDefTypeInNeutral :: (LCType, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
+substDefTypeInNeutral dv p = go
   where
-    go _ e@(LCNeutVar _) = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b -> substituteNormalInNormal 0 a' b
+    go e@(LCNeutVar _) = LCNormNeut e
+    go (LCNeutApp f a) =
+      case go f of
+        LCNormLam _ b -> substituteNormalInNormal a' 0 b
         LCNormTLam _  -> error "Did you really type check this?"
         LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
       where
-        a' = substituteTypeInNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
+        a' = substDefTypeInNormal dv p a
+    go (LCNeutTApp f t) =
+      case go f of
         LCNormLam _ _ -> error "Did you really type check this?"
-        LCNormTLam b  -> substituteTypeInNormal 0 t' b
+        LCNormTLam b  -> substituteTypeInNormal t' 0 b
         LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t'
       where
-        t' = substituteTypeInType m v t
+        t' = substDefTypeInType dv p t
+
+shift :: (LCTerm, Int, Int) -> LCTerm
+shift = shiftMin 0 0
+
+shiftMin :: Int -> Int -> (LCTerm, Int, Int) -> LCTerm
+shiftMin m' n' (v, r, s) = go m' n' v
+  where
+    go _ n (LCVar x)    = LCVar $ if x < n then x else x + s
+    go m n (LCLam t b)  = LCLam (shiftTypeMin m (t, r)) $ go m (n + 1) b
+    go m n (LCApp f a)  = go m n f `LCApp` go m n a
+    go m n (LCTLam b)   = LCTLam $ go (m + 1) n b
+    go m n (LCTApp f t) = go m n f `LCTApp` shiftTypeMin m (t, r)
+
+shiftType :: (LCType, Int) -> LCType
+shiftType = shiftTypeMin 0
+
+shiftTypeMin :: Int -> (LCType, Int) -> LCType
+shiftTypeMin m' (v, r) = go m' v
+  where
+    go _ LCBase      = LCBase
+    go m (LCTVar p)  = LCTVar $ if p < m then p else p + r
+    go m (LCArr a b) = go m a `LCArr` go m b
+    go m (LCUniv a)  = LCUniv $ go (m + 1) a
+
+shiftValue :: (LCValue, Int, Int) -> LCTerm
+shiftValue (v, r, s) = shift (liftLCValue v, r, s)
+
+shiftNormal :: (LCNormalTerm, Int, Int) -> LCNormalTerm
+shiftNormal = shiftNormalMin 0 0
+
+shiftNormalMin :: Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm
+shiftNormalMin m' n' (v, r, s) = go m' n' v
+  where
+    go m n (LCNormLam t b) = LCNormLam (shiftTypeMin m (t, r)) $ go m (n + 1) b
+    go m n (LCNormTLam b)  = LCNormTLam $ go (m + 1) n b
+    go m n (LCNormNeut nt) = LCNormNeut $ shiftNeutralMin m n (nt, r, s)
+
+shiftNeutralMin :: Int -> Int -> (LCNeutralTerm, Int, Int) -> LCNeutralTerm
+shiftNeutralMin m n (v, r, s) = go v
+  where
+    go (LCNeutVar x)    = LCNeutVar $ if x < n then x else x + s
+    go (LCNeutApp f a)  = go f `LCNeutApp` shiftNormalMin m n (a, r, s)
+    go (LCNeutTApp f t) = go f `LCNeutTApp` shiftTypeMin m (t, r)
diff --git a/src/LambdaCube/SystemF/TH.hs b/src/LambdaCube/SystemF/TH.hs
--- a/src/LambdaCube/SystemF/TH.hs
+++ b/src/LambdaCube/SystemF/TH.hs
@@ -1,45 +1,57 @@
 module LambdaCube.SystemF.TH
-  ( lc
+  ( qTerm
+  , qType
   ) where
 
 import           Data.Data                  (Data)
 import           Data.Generics              (extQ)
-import           Data.Text                  (Text)
-import qualified Data.Text                  as Text
+import           LambdaCube.Common.TH
 import           LambdaCube.SystemF.Ast
 import           LambdaCube.SystemF.Parser
 import           Language.Haskell.TH.Lib    (ExpQ, varE)
 import           Language.Haskell.TH.Quote  (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,
-                                             location, mkName)
-import qualified Text.Megaparsec            as P
-import qualified Text.Megaparsec.Error      as PE
+import           Language.Haskell.TH.Syntax (mkName)
 
-lc :: QuasiQuoter
-lc =
+qTerm :: QuasiQuoter
+qTerm =
   QuasiQuoter
-    { quoteExp = expLc
+    { quoteExp = qExpTerm
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-expLc :: String -> ExpQ
-expLc str = do
-  l <- location
-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> dataToExpQ converter e
-    Left err -> fail $ PE.errorBundlePretty err
+qExpTerm :: String -> ExpQ
+qExpTerm = qExpBase pTopTerm converter
   where
     converter :: Data b => b -> Maybe ExpQ
     converter =
-      const Nothing
+      converterBase
       `extQ` quotedMVar
       `extQ` quotedMTVar
-      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
     quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
     quotedMVar _             = Nothing
+
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
+
+qType :: QuasiQuoter
+qType =
+  QuasiQuoter
+    { quoteExp = qExpType
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+qExpType :: String -> ExpQ
+qExpType = qExpBase pTopType converter
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      converterBase
+      `extQ` quotedMTVar
 
     quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
     quotedMTVar _              = Nothing
diff --git a/src/LambdaCube/SystemF/TypeChecker.hs b/src/LambdaCube/SystemF/TypeChecker.hs
--- a/src/LambdaCube/SystemF/TypeChecker.hs
+++ b/src/LambdaCube/SystemF/TypeChecker.hs
@@ -1,4 +1,6 @@
-module LambdaCube.SystemF.TypeChecker where
+module LambdaCube.SystemF.TypeChecker
+  ( infer
+  ) where
 
 import           Data.List                       (uncons)
 import           LambdaCube.SystemF.Ast
@@ -7,7 +9,7 @@
 infer :: LCTerm -> LCType
 infer = go []
   where
-    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl
+    go tl (LCVar x) = maybe (error "Out-of-scope variable") fst . uncons $ drop x tl
     go tl (LCLam t b) = t `LCArr` go (t : tl) b
     go tl (LCApp f a)
       | LCArr at rt <- go tl f
@@ -15,9 +17,9 @@
       = rt
       | otherwise
       = error "Function argument type mismatch"
-    go tl (LCTLam b) = LCUniv $ go tl b
+    go tl (LCTLam b) = LCUniv $ go (fmap (shiftType . (, 1)) tl) b
     go tl (LCTApp f t)
       | LCUniv rt <- go tl f
-      = substituteTypeInType 0 t rt
+      = substituteTypeInType t 0 rt
       | otherwise
       = error "Function argument type mismatch"
diff --git a/src/LambdaCube/SystemFw.hs b/src/LambdaCube/SystemFw.hs
--- a/src/LambdaCube/SystemFw.hs
+++ b/src/LambdaCube/SystemFw.hs
@@ -1,6 +1,7 @@
 module LambdaCube.SystemFw
   ( module LambdaCube.SystemFw.Ast
   , module LambdaCube.SystemFw.Elaborator
+  , module LambdaCube.SystemFw.Evaluator
   , module LambdaCube.SystemFw.Lifter
   , module LambdaCube.SystemFw.Normalizer
   , module LambdaCube.SystemFw.Parser
@@ -13,6 +14,7 @@
 import LambdaCube.SystemFw.Ast
 
 import LambdaCube.SystemFw.Elaborator
+import LambdaCube.SystemFw.Evaluator
 import LambdaCube.SystemFw.Lifter
 import LambdaCube.SystemFw.Normalizer
 import LambdaCube.SystemFw.Parser
diff --git a/src/LambdaCube/SystemFw/Ast.hs b/src/LambdaCube/SystemFw/Ast.hs
--- a/src/LambdaCube/SystemFw/Ast.hs
+++ b/src/LambdaCube/SystemFw/Ast.hs
@@ -4,12 +4,16 @@
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
-data ExtLCKind
-  = ExtLCStar
-  | ExtLCKArr ExtLCKind ExtLCKind
-  | ExtLCMKVar String
+data ExtLCTerm
+  = ExtLCVar Text
+  | ExtLCLam Text ExtLCType ExtLCTerm
+  | ExtLCApp ExtLCTerm ExtLCTerm
+  | ExtLCTLam Text ExtLCKind ExtLCTerm
+  | ExtLCTApp ExtLCTerm ExtLCType
+  | ExtLCMVar String
   deriving stock (Eq, Show, Data, Lift)
-infixr 5 `ExtLCKArr`
+infixl 6 `ExtLCApp`
+infixl 6 `ExtLCTApp`
 
 data ExtLCType
   = ExtLCBase
@@ -23,22 +27,22 @@
 infixr 5 `ExtLCArr`
 infixl 6 `ExtLCTTApp`
 
-data ExtLCTerm
-  = ExtLCVar Text
-  | ExtLCLam Text ExtLCType ExtLCTerm
-  | ExtLCApp ExtLCTerm ExtLCTerm
-  | ExtLCTLam Text ExtLCKind ExtLCTerm
-  | ExtLCTApp ExtLCTerm ExtLCType
-  | ExtLCMVar String
+data ExtLCKind
+  = ExtLCStar
+  | ExtLCKArr ExtLCKind ExtLCKind
+  | ExtLCMKVar String
   deriving stock (Eq, Show, Data, Lift)
-infixl 6 `ExtLCApp`
-infixl 6 `ExtLCTApp`
+infixr 5 `ExtLCKArr`
 
-data LCKind
-  = LCStar
-  | LCKArr LCKind LCKind
+data LCTerm
+  = LCVar Int
+  | LCLam LCType LCTerm
+  | LCApp LCTerm LCTerm
+  | LCTLam LCKind LCTerm
+  | LCTApp LCTerm LCType
   deriving stock (Eq, Show, Data, Lift)
-infixr 5 `LCKArr`
+infixl 6 `LCApp`
+infixl 6 `LCTApp`
 
 data LCType
   = LCBase
@@ -51,15 +55,11 @@
 infixr 5 `LCArr`
 infixl 6 `LCTTApp`
 
-data LCTerm
-  = LCVar Int
-  | LCLam LCType LCTerm
-  | LCApp LCTerm LCTerm
-  | LCTLam LCKind LCTerm
-  | LCTApp LCTerm LCType
+data LCKind
+  = LCStar
+  | LCKArr LCKind LCKind
   deriving stock (Eq, Show, Data, Lift)
-infixl 6 `LCApp`
-infixl 6 `LCTApp`
+infixr 5 `LCKArr`
 
 data LCValue
   = LCValLam LCType LCTerm
diff --git a/src/LambdaCube/SystemFw/Elaborator.hs b/src/LambdaCube/SystemFw/Elaborator.hs
--- a/src/LambdaCube/SystemFw/Elaborator.hs
+++ b/src/LambdaCube/SystemFw/Elaborator.hs
@@ -1,4 +1,8 @@
-module LambdaCube.SystemFw.Elaborator where
+module LambdaCube.SystemFw.Elaborator
+  ( elaborate
+  , elaborateType
+  , elaborateKind
+  ) where
 
 import           Data.List               (elemIndex)
 import           Data.Text               (Text)
@@ -15,7 +19,7 @@
       = error $ "Term variable " <> Text.unpack x <> " is not in scope"
     go tl vl (ExtLCLam x t b) = LCLam (elaborateType tl t) $ go tl (x : vl) b
     go tl vl (ExtLCApp f a) = go tl vl f `LCApp` go tl vl a
-    go tl vl (ExtLCTLam x k b) = LCTLam (elaborateKind k) $ go (x : tl) vl b
+    go tl vl (ExtLCTLam p k b) = LCTLam (elaborateKind k) $ go (p : tl) vl b
     go tl vl (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t
     go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
 
@@ -23,14 +27,14 @@
 elaborateType = go
   where
     go _ ExtLCBase = LCBase
-    go l (ExtLCTVar x)
-      | Just n <- x `elemIndex` l
+    go l (ExtLCTVar p)
+      | Just n <- p `elemIndex` l
       = LCTVar n
       | otherwise
-      = error $ "Type variable " <> Text.unpack x <> " is not in scope"
+      = error $ "Type variable " <> Text.unpack p <> " is not in scope"
     go l (ExtLCArr a b) = go l a `LCArr` go l b
-    go l (ExtLCUniv x k a) = LCUniv (elaborateKind k) $ go (x : l) a
-    go l (ExtLCTTLam x k b) = LCTTLam (elaborateKind k) $ go (x : l) b
+    go l (ExtLCUniv p k a) = LCUniv (elaborateKind k) $ go (p : l) a
+    go l (ExtLCTTLam p k b) = LCTTLam (elaborateKind k) $ go (p : l) b
     go l (ExtLCTTApp f a) = go l f `LCTTApp` go l a
     go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
 
diff --git a/src/LambdaCube/SystemFw/Evaluator.hs b/src/LambdaCube/SystemFw/Evaluator.hs
--- a/src/LambdaCube/SystemFw/Evaluator.hs
+++ b/src/LambdaCube/SystemFw/Evaluator.hs
@@ -1,4 +1,6 @@
-module LambdaCube.SystemFw.Evaluator where
+module LambdaCube.SystemFw.Evaluator
+  ( evaluate
+  ) where
 
 import           LambdaCube.SystemFw.Ast
 import           LambdaCube.SystemFw.Substitution
@@ -11,12 +13,12 @@
     go (LCApp f a)
       | LCValLam _ b <- go f
       , v <- go a
-      = go $ substituteValue 0 v b
+      = go $ substituteValue v 0 b
       | otherwise
       = error "Did you really type check this?"
     go (LCTLam k b) = LCValTLam k b
     go (LCTApp f t)
       | LCValTLam _ b <- go f
-      = go $ substituteType 0 t b
+      = go $ substituteType t 0 b
       | otherwise
       = error "Did you really type check this?"
diff --git a/src/LambdaCube/SystemFw/Lifter.hs b/src/LambdaCube/SystemFw/Lifter.hs
--- a/src/LambdaCube/SystemFw/Lifter.hs
+++ b/src/LambdaCube/SystemFw/Lifter.hs
@@ -1,4 +1,7 @@
-module LambdaCube.SystemFw.Lifter where
+module LambdaCube.SystemFw.Lifter
+  ( liftLCValue
+  , liftLCNormal
+  ) where
 
 import           LambdaCube.SystemFw.Ast
 
@@ -12,6 +15,6 @@
 liftLCNormal (LCNormNeut nt)  = liftLCNeutral nt
 
 liftLCNeutral :: LCNeutralTerm -> LCTerm
-liftLCNeutral (LCNeutVar n)    = LCVar n
+liftLCNeutral (LCNeutVar x)    = LCVar x
 liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a
 liftLCNeutral (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
diff --git a/src/LambdaCube/SystemFw/Normalizer.hs b/src/LambdaCube/SystemFw/Normalizer.hs
--- a/src/LambdaCube/SystemFw/Normalizer.hs
+++ b/src/LambdaCube/SystemFw/Normalizer.hs
@@ -1,4 +1,6 @@
-module LambdaCube.SystemFw.Normalizer where
+module LambdaCube.SystemFw.Normalizer
+  ( normalize
+  ) where
 
 import           LambdaCube.SystemFw.Ast
 import           LambdaCube.SystemFw.Substitution
@@ -6,18 +8,18 @@
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
   where
-    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCVar x) = LCNormNeut $ LCNeutVar x
     go (LCLam t b) = LCNormLam t $ go b
     go (LCTLam k b) = LCNormTLam k $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
-        LCNormTLam _ _  -> error "Did you really type check this?"
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+        LCNormLam _ b  -> substituteNormalInNormal a' 0 b
+        LCNormTLam _ _ -> error "Did you really type check this?"
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
       where
         a' = go a
     go (LCTApp f t) =
       case go f of
-        LCNormLam _ _   -> error "Did you really type check this?"
-        LCNormTLam _ b  -> substituteTypeInNormal 0 t b
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
+        LCNormLam _ _  -> error "Did you really type check this?"
+        LCNormTLam _ b -> substituteTypeInNormal t 0 b
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t
diff --git a/src/LambdaCube/SystemFw/Parser.hs b/src/LambdaCube/SystemFw/Parser.hs
--- a/src/LambdaCube/SystemFw/Parser.hs
+++ b/src/LambdaCube/SystemFw/Parser.hs
@@ -1,4 +1,8 @@
-module LambdaCube.SystemFw.Parser where
+module LambdaCube.SystemFw.Parser
+  ( pTopTerm
+  , pTopType
+  , pTopKind
+  ) where
 
 import           Data.Foldable            (Foldable (foldl'))
 import           Data.Function            ((&))
@@ -9,25 +13,25 @@
 import           LambdaCube.SystemFw.Ast
 import           Text.Megaparsec
 
-pTopLC :: Parser ExtLCTerm
-pTopLC = topParser pLC
+pTopTerm :: Parser ExtLCTerm
+pTopTerm = topParser pTerm
 
-pLC :: Parser ExtLCTerm
-pLC = pTLam <|> pLam <|> pApp
+pTerm :: Parser ExtLCTerm
+pTerm = pTLam <|> pLam <|> pApp
 
 pTLam :: Parser ExtLCTerm
 pTLam =
   ExtLCTLam
   <$> (atsignBackslash *> identifier)
   <*> (colon *> pKind)
-  <*> (dot *> pLC)
+  <*> (dot *> pTerm)
 
 pLam :: Parser ExtLCTerm
 pLam =
   ExtLCLam
   <$> (backslash *> identifier)
   <*> (colon *> pType)
-  <*> (dot *> pLC)
+  <*> (dot *> pTerm)
 
 pApp :: Parser ExtLCTerm
 pApp = foldl' (&) <$> pATerm <*> many pAppArg
@@ -40,7 +44,7 @@
     else flip ExtLCApp <$> pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = pVar <|> pMVar <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pTerm
 
 pVar :: Parser ExtLCTerm
 pVar = ExtLCVar <$> identifier
@@ -48,6 +52,9 @@
 pMVar :: Parser ExtLCTerm
 pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
 
+pTopType :: Parser ExtLCType
+pTopType = topParser pType
+
 pType :: Parser ExtLCType
 pType = pTTLam <|> pUniv <|> pArr
 
@@ -82,6 +89,9 @@
 
 pMTVar :: Parser ExtLCType
 pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
+
+pTopKind :: Parser ExtLCKind
+pTopKind = topParser pKind
 
 pKind :: Parser ExtLCKind
 pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow
diff --git a/src/LambdaCube/SystemFw/PrettyPrinter.hs b/src/LambdaCube/SystemFw/PrettyPrinter.hs
--- a/src/LambdaCube/SystemFw/PrettyPrinter.hs
+++ b/src/LambdaCube/SystemFw/PrettyPrinter.hs
@@ -2,28 +2,50 @@
   TODO: Use real pretty printer library
 -}
 {-# LANGUAGE OverloadedStrings #-}
-module LambdaCube.SystemFw.PrettyPrinter where
+module LambdaCube.SystemFw.PrettyPrinter
+  ( prettyUnnamedTerm
+  , prettyShowUnnamedTerm
+  , prettyUnnamedType
+  , prettyShowUnnamedType
+  , prettyUnnamedKind
+  , prettyShowUnnamedKind
+  ) where
 
 import           Data.Text                       (Text)
 import qualified Data.Text                       as Text
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.SystemFw.Ast
 
-prettyUnnamedKind :: LCKind -> Text
-prettyUnnamedKind = prettyUnnamedKindPrec 0
+prettyUnnamedTerm :: LCTerm -> Text
+prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
+prettyShowUnnamedTerm :: LCTerm -> String
+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm
+
 prettyUnnamedType :: LCType -> Text
 prettyUnnamedType = prettyUnnamedTypePrec 0
 
-prettyUnnamedTerm :: LCTerm -> Text
-prettyUnnamedTerm = prettyUnnamedTermPrec 0
+prettyShowUnnamedType :: LCType -> String
+prettyShowUnnamedType = Text.unpack . prettyUnnamedType
 
-prettyUnnamedKindPrec :: Int -> LCKind -> Text
-prettyUnnamedKindPrec = go
+prettyUnnamedKind :: LCKind -> Text
+prettyUnnamedKind = prettyUnnamedKindPrec 0
+
+prettyShowUnnamedKind :: LCKind -> String
+prettyShowUnnamedKind = Text.unpack . prettyUnnamedKind
+
+prettyUnnamedTermPrec :: Int -> LCTerm -> Text
+prettyUnnamedTermPrec = go
   where
-    go _ LCStar       = "*"
-    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+    pKP = prettyUnnamedKindPrec
+    pTP = prettyUnnamedTypePrec
 
+    go _ (LCVar i)    = Text.pack $ show i
+    go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+    go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+    go p (LCTLam k b) = wrapIfSpaced (p > 0) ["@\\ :", pKP 0 k, ".", go 0 b]
+    go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]
+
 prettyUnnamedTypePrec :: Int -> LCType -> Text
 prettyUnnamedTypePrec = go
   where
@@ -36,14 +58,8 @@
     go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]
     go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
 
-prettyUnnamedTermPrec :: Int -> LCTerm -> Text
-prettyUnnamedTermPrec = go
+prettyUnnamedKindPrec :: Int -> LCKind -> Text
+prettyUnnamedKindPrec = go
   where
-    pKP = prettyUnnamedKindPrec
-    pTP = prettyUnnamedTypePrec
-
-    go _ (LCVar i)    = Text.pack $ show i
-    go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
-    go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
-    go p (LCTLam k b) = wrapIfSpaced (p > 0) ["@\\ :", pKP 0 k, ".", go 0 b]
-    go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]
+    go _ LCStar       = "*"
+    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
diff --git a/src/LambdaCube/SystemFw/Substitution.hs b/src/LambdaCube/SystemFw/Substitution.hs
--- a/src/LambdaCube/SystemFw/Substitution.hs
+++ b/src/LambdaCube/SystemFw/Substitution.hs
@@ -1,84 +1,154 @@
-module LambdaCube.SystemFw.Substitution where
+{-# LANGUAGE ViewPatterns #-}
+module LambdaCube.SystemFw.Substitution
+  ( substituteType
+  , substituteTypeInType
+  , substituteValue
+  , substituteNormalInNormal
+  , substituteTypeInNormal
 
+  , shiftType
+  ) where
+
 import           LambdaCube.SystemFw.Ast
 import           LambdaCube.SystemFw.Lifter
 
-substituteType :: Int -> LCType -> LCTerm -> LCTerm
-substituteType n v = go n
+substituteType :: LCType -> Int -> LCTerm -> LCTerm
+substituteType v = substDefType (v, 0)
+
+substituteTypeInType :: LCType -> Int -> LCType -> LCType
+substituteTypeInType v = substDefTypeInType (v, 0)
+
+substituteValue :: LCValue -> Int -> LCTerm -> LCTerm
+substituteValue v = substDefValue (v, 0, 0)
+
+substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal v = substDefNormalInNormal (v, 0, 0)
+
+substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm
+substituteTypeInNormal v = substDefTypeInNormal (v, 0)
+
+substDefType :: (LCType, Int) -> Int -> LCTerm -> LCTerm
+substDefType = go
   where
-    go _ e@(LCVar _)  = e
-    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam k b) = LCTLam k $ go (m + 1) b
-    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
+    go _      _ e@(LCVar _)  = e
+    go dv     p (LCLam t b)  = LCLam (substDefTypeInType dv p t) $ go dv p b
+    go dv     p (LCApp f a)  = go dv p f `LCApp` go dv p a
+    go (v, r) p (LCTLam k b) = LCTLam k $ go (v, r + 1) (p + 1) b
+    go dv     p (LCTApp f t) = go dv p f `LCTApp` substDefTypeInType dv p t
 
-substituteTypeInType :: Int -> LCType -> LCType -> LCType
-substituteTypeInType n v = go n
+substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType
+substDefTypeInType = go
   where
-    go _ LCBase        = LCBase
-    go m e@(LCTVar l)  = if m == l then v else e
-    go m (LCArr a b)   = go m a `LCArr` go m b
-    go m (LCUniv k a)  = LCUniv k $ go (m + 1) a
-    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
-    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+    go _      _ LCBase                     = LCBase
+    go dv     p (LCTVar ((== p) -> True))  = shiftType dv
+    go _      p e@(LCTVar ((< p) -> True)) = e
+    go _      _ (LCTVar q)                 = LCTVar $ q - 1
+    go dv     p (LCArr a b)                = go dv p a `LCArr` go dv p b
+    go (v, r) p (LCUniv k a)               = LCUniv k $ go (v, r + 1) (p + 1) a
+    go (v, r) p (LCTTLam k b)              = LCTTLam k $ go (v, r + 1) (p + 1) b
+    go dv     p (LCTTApp f a)              = go dv p f `LCTTApp` go dv p a
 
-substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
-substituteValue n v = go n
+substDefValue :: (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm
+substDefValue = go
   where
-    go m e@(LCVar l)  = if m == l then liftLCValue v else e
-    go m (LCLam t b)  = LCLam t $ go (m + 1) b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam k b) = LCTLam k $ go m b
-    go m (LCTApp f t) = go m f `LCTApp` t
+    go dv        x (LCVar ((== x) -> True))  = shiftValue dv
+    go _         x e@(LCVar ((< x) -> True)) = e
+    go _         _ (LCVar y)                 = LCVar $ y - 1
+    go (v, r, s) x (LCLam t b)  = LCLam t $ go (v, r, s + 1) (x + 1) b
+    go dv        x (LCApp f a)  = go dv x f `LCApp` go dv x a
+    go (v, r, s) x (LCTLam k b) = LCTLam k $ go (v, r + 1, s) x b
+    go dv        x (LCTApp f t) = go dv x f `LCTApp` t
 
-substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormalInNormal n v = go n
+substDefNormalInNormal :: (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm
+substDefNormalInNormal = go
   where
-    go m (LCNormLam t b)  = LCNormLam t $ go (m + 1) b
-    go m (LCNormTLam k b) = LCNormTLam k $ go m b
-    go m (LCNormNeut nt)  = substituteNormalInNeutral m v nt
+    go (v, r, s) x (LCNormLam t b)  = LCNormLam t $ go (v, r, s + 1) (x + 1) b
+    go (v, r, s) x (LCNormTLam k b) = LCNormTLam k $ go (v, r + 1, s) x b
+    go dv        x (LCNormNeut nt)  = substDefNormalInNeutral dv x nt
 
-substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNormalInNeutral n v = go n
+substDefNormalInNeutral :: (LCNormalTerm, Int, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
+substDefNormalInNeutral dv x = go
   where
-    go m e@(LCNeutVar l)
-      | m == l = v
-      | otherwise = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b  -> substituteNormalInNormal 0 a' b
+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv
+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e
+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1
+    go (LCNeutApp f a) =
+      case go f of
+        LCNormLam _ b  -> substituteNormalInNormal a' 0 b
         LCNormTLam _ _ -> error "Did you really type check this?"
         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
       where
-        a' = substituteNormalInNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
+        a' = substDefNormalInNormal dv x a
+    go (LCNeutTApp f t) =
+      case go f of
         LCNormLam _ _  -> error "Did you really type check this?"
-        LCNormTLam _ b -> substituteTypeInNormal 0 t b
+        LCNormTLam _ b -> substituteTypeInNormal t 0 b
         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t
 
-substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
-substituteTypeInNormal n v = go n
+substDefTypeInNormal :: (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm
+substDefTypeInNormal = go
   where
-    go m (LCNormLam t b)  = LCNormLam (substituteTypeInType m v t) $ go m b
-    go m (LCNormTLam k b) = LCNormTLam k $ go (m + 1) b
-    go m (LCNormNeut nt)  = substituteTypeInNeutral m v nt
+    go dv     p (LCNormLam t b)  = LCNormLam (substDefTypeInType dv p t) $ go dv p b
+    go (v, r) p (LCNormTLam k b) = LCNormTLam k $ go (v, r + 1) (p + 1) b
+    go dv     p (LCNormNeut nt)  = substDefTypeInNeutral dv p nt
 
-substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
-substituteTypeInNeutral n v = go n
+substDefTypeInNeutral :: (LCType, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
+substDefTypeInNeutral dv p = go
   where
-    go _ e@(LCNeutVar _) = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b  -> substituteNormalInNormal 0 a' b
+    go e@(LCNeutVar _) = LCNormNeut e
+    go (LCNeutApp f a) =
+      case go f of
+        LCNormLam _ b  -> substituteNormalInNormal a' 0 b
         LCNormTLam _ _ -> error "Did you really type check this?"
         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
       where
-        a' = substituteTypeInNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
+        a' = substDefTypeInNormal dv p a
+    go (LCNeutTApp f t) =
+      case go f of
         LCNormLam _ _  -> error "Did you really type check this?"
-        LCNormTLam _ b -> substituteTypeInNormal 0 t' b
+        LCNormTLam _ b -> substituteTypeInNormal t' 0 b
         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t'
       where
-        t' = substituteTypeInType m v t
+        t' = substDefTypeInType dv p t
+
+shift :: (LCTerm, Int, Int) -> LCTerm
+shift (v, r, s) = go 0 0 v
+  where
+    go _ n (LCVar x)    = LCVar $ if x < n then x else x + s
+    go m n (LCLam t b)  = LCLam (shiftTypeMin m (t, r)) $ go m (n + 1) b
+    go m n (LCApp f a)  = go m n f `LCApp` go m n a
+    go m n (LCTLam k b) = LCTLam k $ go (m + 1) n b
+    go m n (LCTApp f t) = go m n f `LCTApp` shiftTypeMin m (t, r)
+
+shiftType :: (LCType, Int) -> LCType
+shiftType = shiftTypeMin 0
+
+shiftTypeMin :: Int -> (LCType, Int) -> LCType
+shiftTypeMin m' (v, r) = go m' v
+  where
+    go _ LCBase        = LCBase
+    go m (LCTVar p)    = LCTVar $ if p < m then p else p + r
+    go m (LCArr a b)   = go m a `LCArr` go m b
+    go m (LCUniv k a)  = LCUniv k $ go (m + 1) a
+    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
+    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+
+shiftValue :: (LCValue, Int, Int) -> LCTerm
+shiftValue (v, r, s) = shift (liftLCValue v, r, s)
+
+shiftNormal :: (LCNormalTerm, Int, Int) -> LCNormalTerm
+shiftNormal = shiftNormalMin 0 0
+
+shiftNormalMin :: Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm
+shiftNormalMin m' n' (v, r, s) = go m' n' v
+  where
+    go m n (LCNormLam t b)  = LCNormLam (shiftTypeMin m (t, r)) $ go m (n + 1) b
+    go m n (LCNormTLam k b) = LCNormTLam k $ go (m + 1) n b
+    go m n (LCNormNeut nt)  = LCNormNeut $ shiftNeutralMin m n (nt, r, s)
+
+shiftNeutralMin :: Int -> Int -> (LCNeutralTerm, Int, Int) -> LCNeutralTerm
+shiftNeutralMin m n (v, r, s) = go v
+  where
+    go (LCNeutVar x)    = LCNeutVar $ if x < n then x else x + s
+    go (LCNeutApp f a)  = go f `LCNeutApp` shiftNormalMin m n (a, r, s)
+    go (LCNeutTApp f t) = go f `LCNeutTApp` shiftTypeMin m (t, r)
diff --git a/src/LambdaCube/SystemFw/TH.hs b/src/LambdaCube/SystemFw/TH.hs
--- a/src/LambdaCube/SystemFw/TH.hs
+++ b/src/LambdaCube/SystemFw/TH.hs
@@ -1,49 +1,86 @@
 module LambdaCube.SystemFw.TH
-  ( lc
+  ( qTerm
+  , qType
+  , qKind
   ) where
 
 import           Data.Data                  (Data)
 import           Data.Generics              (extQ)
-import           Data.Text                  (Text)
-import qualified Data.Text                  as Text
+import           LambdaCube.Common.TH
 import           LambdaCube.SystemFw.Ast
 import           LambdaCube.SystemFw.Parser
 import           Language.Haskell.TH.Lib    (ExpQ, varE)
 import           Language.Haskell.TH.Quote  (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,
-                                             location, mkName)
-import qualified Text.Megaparsec            as P
-import qualified Text.Megaparsec.Error      as PE
+import           Language.Haskell.TH.Syntax (mkName)
 
-lc :: QuasiQuoter
-lc =
+qTerm :: QuasiQuoter
+qTerm =
   QuasiQuoter
-    { quoteExp = expLc
+    { quoteExp = qExpTerm
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-expLc :: String -> ExpQ
-expLc str = do
-  l <- location
-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> dataToExpQ converter e
-    Left err -> fail $ PE.errorBundlePretty err
+qExpTerm :: String -> ExpQ
+qExpTerm = qExpBase pTopTerm converter
   where
     converter :: Data b => b -> Maybe ExpQ
     converter =
-      const Nothing
+      converterBase
       `extQ` quotedMVar
       `extQ` quotedMTVar
       `extQ` quotedMKVar
-      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
     quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
     quotedMVar _             = Nothing
 
     quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
     quotedMTVar _              = Nothing
+
+    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
+    quotedMKVar _              = Nothing
+
+qType :: QuasiQuoter
+qType =
+  QuasiQuoter
+    { quoteExp = qExpType
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+qExpType :: String -> ExpQ
+qExpType = qExpBase pTopType converter
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      converterBase
+      `extQ` quotedMTVar
+      `extQ` quotedMKVar
+
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
+
+    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
+    quotedMKVar _              = Nothing
+
+qKind :: QuasiQuoter
+qKind =
+  QuasiQuoter
+    { quoteExp = qExpKind
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+qExpKind :: String -> ExpQ
+qExpKind = qExpBase pTopKind converter
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      converterBase
+      `extQ` quotedMKVar
 
     quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
     quotedMKVar _              = Nothing
diff --git a/src/LambdaCube/SystemFw/TypeChecker.hs b/src/LambdaCube/SystemFw/TypeChecker.hs
--- a/src/LambdaCube/SystemFw/TypeChecker.hs
+++ b/src/LambdaCube/SystemFw/TypeChecker.hs
@@ -1,5 +1,10 @@
-module LambdaCube.SystemFw.TypeChecker where
+module LambdaCube.SystemFw.TypeChecker
+  ( reduceType
 
+  , infer
+  , inferKind
+  ) where
+
 import           Data.List                        (uncons)
 import           LambdaCube.SystemFw.Ast
 import           LambdaCube.SystemFw.Substitution
@@ -15,37 +20,39 @@
     go (LCTTApp f a)
       | LCTTLam _ b <- go f
       , v <- go a
-      = go $ substituteTypeInType 0 v b
+      = go $ substituteTypeInType v 0 b
       | otherwise
       = error "Did you really kind check this?"
 
 infer :: LCTerm -> LCType
-infer = go []
+infer = go [] []
   where
-    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl
-    go tl (LCLam t b)
-      | LCStar <- inferKind t
-      = v `LCArr` go (v : tl) b
+    go _  tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl
+    go kl tl (LCLam t b)
+      | LCStar <- inferKind kl t
+      = v `LCArr` go kl (v : tl) b
       | otherwise
       = error "Function argument kind mismatch"
       where
         v = reduceType t
-    go tl (LCApp f a)
-      | LCArr at rt <- go tl f
-      , at == go tl a
+    go kl tl (LCApp f a)
+      | LCArr at rt <- go kl tl f
+      , at == go kl tl a
       = rt
       | otherwise
       = error "Function argument type mismatch"
-    go tl (LCTLam k b) = LCUniv k $ go tl b
-    go tl (LCTApp f t)
-      | LCUniv tk rt <- go tl f
-      , tk == inferKind t
-      = substituteTypeInType 0 t rt
+    go kl tl (LCTLam k b) = LCUniv k $ go (k : kl) (fmap (shiftType . (, 1)) tl) b
+    go kl tl (LCTApp f t)
+      | LCUniv tk rt <- go kl tl f
+      , tk == inferKind kl t
+      = substituteTypeInType v 0 rt
       | otherwise
       = error "Function argument kind mismatch"
+      where
+        v = reduceType t
 
-inferKind :: LCType -> LCKind
-inferKind = go []
+inferKind :: [LCKind] -> LCType -> LCKind
+inferKind = go
   where
     go _  LCBase = LCStar
     go kl (LCTVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n kl
diff --git a/src/LambdaCube/SystemFw_.hs b/src/LambdaCube/SystemFw_.hs
--- a/src/LambdaCube/SystemFw_.hs
+++ b/src/LambdaCube/SystemFw_.hs
@@ -1,6 +1,7 @@
 module LambdaCube.SystemFw_
   ( module LambdaCube.SystemFw_.Ast
   , module LambdaCube.SystemFw_.Elaborator
+  , module LambdaCube.SystemFw_.Evaluator
   , module LambdaCube.SystemFw_.Lifter
   , module LambdaCube.SystemFw_.Normalizer
   , module LambdaCube.SystemFw_.Parser
@@ -13,6 +14,7 @@
 import LambdaCube.SystemFw_.Ast
 
 import LambdaCube.SystemFw_.Elaborator
+import LambdaCube.SystemFw_.Evaluator
 import LambdaCube.SystemFw_.Lifter
 import LambdaCube.SystemFw_.Normalizer
 import LambdaCube.SystemFw_.Parser
diff --git a/src/LambdaCube/SystemFw_/Ast.hs b/src/LambdaCube/SystemFw_/Ast.hs
--- a/src/LambdaCube/SystemFw_/Ast.hs
+++ b/src/LambdaCube/SystemFw_/Ast.hs
@@ -4,12 +4,13 @@
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
-data ExtLCKind
-  = ExtLCStar
-  | ExtLCKArr ExtLCKind ExtLCKind
-  | ExtLCMKVar String
+data ExtLCTerm
+  = ExtLCVar Text
+  | ExtLCLam Text ExtLCType ExtLCTerm
+  | ExtLCApp ExtLCTerm ExtLCTerm
+  | ExtLCMVar String
   deriving stock (Eq, Show, Data, Lift)
-infixr 5 `ExtLCKArr`
+infixl 6 `ExtLCApp`
 
 data ExtLCType
   = ExtLCBase
@@ -22,19 +23,19 @@
 infixr 5 `ExtLCArr`
 infixl 6 `ExtLCTTApp`
 
-data ExtLCTerm
-  = ExtLCVar Text
-  | ExtLCLam Text ExtLCType ExtLCTerm
-  | ExtLCApp ExtLCTerm ExtLCTerm
-  | ExtLCMVar String
+data ExtLCKind
+  = ExtLCStar
+  | ExtLCKArr ExtLCKind ExtLCKind
+  | ExtLCMKVar String
   deriving stock (Eq, Show, Data, Lift)
-infixl 6 `ExtLCApp`
+infixr 5 `ExtLCKArr`
 
-data LCKind
-  = LCStar
-  | LCKArr LCKind LCKind
+data LCTerm
+  = LCVar Int
+  | LCLam LCType LCTerm
+  | LCApp LCTerm LCTerm
   deriving stock (Eq, Show, Data, Lift)
-infixr 5 `LCKArr`
+infixl 6 `LCApp`
 
 data LCType
   = LCBase
@@ -46,12 +47,11 @@
 infixr 5 `LCArr`
 infixl 6 `LCTTApp`
 
-data LCTerm
-  = LCVar Int
-  | LCLam LCType LCTerm
-  | LCApp LCTerm LCTerm
+data LCKind
+  = LCStar
+  | LCKArr LCKind LCKind
   deriving stock (Eq, Show, Data, Lift)
-infixl 6 `LCApp`
+infixr 5 `LCKArr`
 
 data LCValue
   = LCValLam LCType LCTerm
diff --git a/src/LambdaCube/SystemFw_/Elaborator.hs b/src/LambdaCube/SystemFw_/Elaborator.hs
--- a/src/LambdaCube/SystemFw_/Elaborator.hs
+++ b/src/LambdaCube/SystemFw_/Elaborator.hs
@@ -1,4 +1,8 @@
-module LambdaCube.SystemFw_.Elaborator where
+module LambdaCube.SystemFw_.Elaborator
+  ( elaborate
+  , elaborateType
+  , elaborateKind
+  ) where
 
 import           Data.List                (elemIndex)
 import qualified Data.Text                as Text
@@ -20,13 +24,13 @@
 elaborateType = go []
   where
     go _ ExtLCBase = LCBase
-    go l (ExtLCTVar x)
-      | Just n <- x `elemIndex` l
+    go l (ExtLCTVar p)
+      | Just n <- p `elemIndex` l
       = LCTVar n
       | otherwise
-      = error $ "Type variable " <> Text.unpack x <> " is not in scope"
+      = error $ "Type variable " <> Text.unpack p <> " is not in scope"
     go l (ExtLCArr a b) = go l a `LCArr` go l b
-    go l (ExtLCTTLam x k b) = LCTTLam (elaborateKind k) $ go (x : l) b
+    go l (ExtLCTTLam p k b) = LCTTLam (elaborateKind k) $ go (p : l) b
     go l (ExtLCTTApp f a) = go l f `LCTTApp` go l a
     go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
 
diff --git a/src/LambdaCube/SystemFw_/Evaluator.hs b/src/LambdaCube/SystemFw_/Evaluator.hs
--- a/src/LambdaCube/SystemFw_/Evaluator.hs
+++ b/src/LambdaCube/SystemFw_/Evaluator.hs
@@ -1,4 +1,6 @@
-module LambdaCube.SystemFw_.Evaluator where
+module LambdaCube.SystemFw_.Evaluator
+  ( evaluate
+  ) where
 
 import           LambdaCube.SystemFw_.Ast
 import           LambdaCube.SystemFw_.Substitution
@@ -11,6 +13,6 @@
     go (LCApp f a)
       | LCValLam _ b <- go f
       , v <- go a
-      = go (substituteValue 0 v b)
+      = go $ substituteValue v 0 b
       | otherwise
       = error "Did you really type check this?"
diff --git a/src/LambdaCube/SystemFw_/Lifter.hs b/src/LambdaCube/SystemFw_/Lifter.hs
--- a/src/LambdaCube/SystemFw_/Lifter.hs
+++ b/src/LambdaCube/SystemFw_/Lifter.hs
@@ -1,14 +1,17 @@
-module LambdaCube.SystemFw_.Lifter where
+module LambdaCube.SystemFw_.Lifter
+  ( liftLCValue
+  , liftLCNormal
+  ) where
 
-import LambdaCube.SystemFw_.Ast
+import           LambdaCube.SystemFw_.Ast
 
 liftLCValue :: LCValue -> LCTerm
 liftLCValue (LCValLam t b) = LCLam t b
 
 liftLCNormal :: LCNormalTerm -> LCTerm
-liftLCNormal (LCNormLam t b)  = LCLam t $ liftLCNormal b
-liftLCNormal (LCNormNeut nt)  = liftLCNeutral nt
+liftLCNormal (LCNormLam t b) = LCLam t $ liftLCNormal b
+liftLCNormal (LCNormNeut nt) = liftLCNeutral nt
 
 liftLCNeutral :: LCNeutralTerm -> LCTerm
-liftLCNeutral (LCNeutVar n)    = LCVar n
-liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a
+liftLCNeutral (LCNeutVar x)   = LCVar x
+liftLCNeutral (LCNeutApp f a) = liftLCNeutral f `LCApp` liftLCNormal a
diff --git a/src/LambdaCube/SystemFw_/Normalizer.hs b/src/LambdaCube/SystemFw_/Normalizer.hs
--- a/src/LambdaCube/SystemFw_/Normalizer.hs
+++ b/src/LambdaCube/SystemFw_/Normalizer.hs
@@ -1,4 +1,6 @@
-module LambdaCube.SystemFw_.Normalizer where
+module LambdaCube.SystemFw_.Normalizer
+  ( normalize
+  ) where
 
 import           LambdaCube.SystemFw_.Ast
 import           LambdaCube.SystemFw_.Substitution
@@ -7,11 +9,11 @@
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
   where
-    go (LCVar n) = LCNormNeut $ LCNeutVar n
+    go (LCVar x) = LCNormNeut $ LCNeutVar x
     go (LCLam t b) = LCNormLam (reduceType t) $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+        LCNormLam _ b -> substituteNormalInNormal a' 0 b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
       where
         a' = go a
diff --git a/src/LambdaCube/SystemFw_/Parser.hs b/src/LambdaCube/SystemFw_/Parser.hs
--- a/src/LambdaCube/SystemFw_/Parser.hs
+++ b/src/LambdaCube/SystemFw_/Parser.hs
@@ -1,4 +1,8 @@
-module LambdaCube.SystemFw_.Parser where
+module LambdaCube.SystemFw_.Parser
+  ( pTopTerm
+  , pTopType
+  , pTopKind
+  ) where
 
 import           Data.Foldable            (Foldable (foldl'))
 import           Data.Functor             (($>))
@@ -7,24 +11,24 @@
 import           LambdaCube.SystemFw_.Ast
 import           Text.Megaparsec
 
-pTopLC :: Parser ExtLCTerm
-pTopLC = topParser pLC
+pTopTerm :: Parser ExtLCTerm
+pTopTerm = topParser pTerm
 
-pLC :: Parser ExtLCTerm
-pLC = pLam <|> pApp
+pTerm :: Parser ExtLCTerm
+pTerm = pLam <|> pApp
 
 pLam :: Parser ExtLCTerm
 pLam =
   ExtLCLam
   <$> (backslash *> identifier)
   <*> (colon *> pType)
-  <*> (dot *> pLC)
+  <*> (dot *> pTerm)
 
 pApp :: Parser ExtLCTerm
 pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = pVar <|> pMVar <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pTerm
 
 pVar :: Parser ExtLCTerm
 pVar = ExtLCVar <$> identifier
@@ -32,6 +36,9 @@
 pMVar :: Parser ExtLCTerm
 pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
 
+pTopType :: Parser ExtLCType
+pTopType = topParser pType
+
 pType :: Parser ExtLCType
 pType = pTTLam <|> pArr
 
@@ -59,6 +66,9 @@
 
 pMTVar :: Parser ExtLCType
 pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
+
+pTopKind :: Parser ExtLCKind
+pTopKind = topParser pKind
 
 pKind :: Parser ExtLCKind
 pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow
diff --git a/src/LambdaCube/SystemFw_/PrettyPrinter.hs b/src/LambdaCube/SystemFw_/PrettyPrinter.hs
--- a/src/LambdaCube/SystemFw_/PrettyPrinter.hs
+++ b/src/LambdaCube/SystemFw_/PrettyPrinter.hs
@@ -2,44 +2,60 @@
   TODO: Use real pretty printer library
 -}
 {-# LANGUAGE OverloadedStrings #-}
-module LambdaCube.SystemFw_.PrettyPrinter where
+module LambdaCube.SystemFw_.PrettyPrinter
+  ( prettyUnnamedTerm
+  , prettyShowUnnamedTerm
+  , prettyUnnamedType
+  , prettyShowUnnamedType
+  , prettyUnnamedKind
+  , prettyShowUnnamedKind
+  ) where
 
 import           Data.Text                       (Text)
 import qualified Data.Text                       as Text
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.SystemFw_.Ast
 
-prettyUnnamedKind :: LCKind -> Text
-prettyUnnamedKind = prettyUnnamedKindPrec 0
+prettyUnnamedTerm :: LCTerm -> Text
+prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
+prettyShowUnnamedTerm :: LCTerm -> String
+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm
+
 prettyUnnamedType :: LCType -> Text
 prettyUnnamedType = prettyUnnamedTypePrec 0
 
-prettyUnnamedTerm :: LCTerm -> Text
-prettyUnnamedTerm = prettyUnnamedTermPrec 0
+prettyShowUnnamedType :: LCType -> String
+prettyShowUnnamedType = Text.unpack . prettyUnnamedType
 
-prettyUnnamedKindPrec :: Int -> LCKind -> Text
-prettyUnnamedKindPrec = go
+prettyUnnamedKind :: LCKind -> Text
+prettyUnnamedKind = prettyUnnamedKindPrec 0
+
+prettyShowUnnamedKind :: LCKind -> String
+prettyShowUnnamedKind = Text.unpack . prettyUnnamedKind
+
+prettyUnnamedTermPrec :: Int -> LCTerm -> Text
+prettyUnnamedTermPrec = go
   where
-    go _ LCStar       = "*"
-    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
+    pTP = prettyUnnamedTypePrec
 
+    go _ (LCVar x)   = Text.pack $ show x
+    go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+    go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+
 prettyUnnamedTypePrec :: Int -> LCType -> Text
 prettyUnnamedTypePrec = go
   where
     pKP = prettyUnnamedKindPrec
 
     go _ LCBase        = "#"
-    go _ (LCTVar i)    = Text.pack $ show i
+    go _ (LCTVar p)    = Text.pack $ show p
     go p (LCArr a b)   = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
     go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]
     go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
 
-prettyUnnamedTermPrec :: Int -> LCTerm -> Text
-prettyUnnamedTermPrec = go
+prettyUnnamedKindPrec :: Int -> LCKind -> Text
+prettyUnnamedKindPrec = go
   where
-    pTP = prettyUnnamedTypePrec
-
-    go _ (LCVar i)   = Text.pack $ show i
-    go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
-    go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
+    go _ LCStar       = "*"
+    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
diff --git a/src/LambdaCube/SystemFw_/Substitution.hs b/src/LambdaCube/SystemFw_/Substitution.hs
--- a/src/LambdaCube/SystemFw_/Substitution.hs
+++ b/src/LambdaCube/SystemFw_/Substitution.hs
@@ -1,37 +1,94 @@
-module LambdaCube.SystemFw_.Substitution where
+{-# LANGUAGE ViewPatterns #-}
+module LambdaCube.SystemFw_.Substitution
+  ( substituteTypeInType
+  , substituteValue
+  , substituteNormalInNormal
+  ) where
 
 import           LambdaCube.SystemFw_.Ast
 import           LambdaCube.SystemFw_.Lifter
 
-substituteTypeInType :: Int -> LCType -> LCType -> LCType
-substituteTypeInType n v = go n
+substituteTypeInType :: LCType -> Int -> LCType -> LCType
+substituteTypeInType v = substDefTypeInType (v, 0)
+
+substituteValue :: LCValue -> Int -> LCTerm -> LCTerm
+substituteValue v = substDefValue (v, 0)
+
+substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal v = substDefNormalInNormal (v, 0)
+
+substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType
+substDefTypeInType = go
   where
+    go _      _ LCBase                     = LCBase
+    go dv     p (LCTVar ((== p) -> True))  = shiftType dv
+    go _      p e@(LCTVar ((< p) -> True)) = e
+    go _      _ (LCTVar q)                 = LCTVar $ q - 1
+    go dv     p (LCArr a b)                = go dv p a `LCArr` go dv p b
+    go (v, r) p (LCTTLam k b)              = LCTTLam k $ go (v, r + 1) (p + 1) b
+    go dv     p (LCTTApp f a)              = go dv p f `LCTTApp` go dv p a
+
+substDefValue :: (LCValue, Int) -> Int -> LCTerm -> LCTerm
+substDefValue = go
+  where
+    go dv     x (LCVar ((== x) -> True))  = shiftValue dv
+    go _      x e@(LCVar ((< x) -> True)) = e
+    go _      _ (LCVar y)                 = LCVar $ y - 1
+    go (v, s) x (LCLam t b)               = LCLam t $ go (v, s + 1) (x + 1) b
+    go dv     x (LCApp f a)               = go dv x f `LCApp` go dv x a
+
+substDefNormalInNormal :: (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm
+substDefNormalInNormal = go
+  where
+    go (v, s) x (LCNormLam t b) = LCNormLam t $ go (v, s + 1) (x + 1) b
+    go dv     x (LCNormNeut nt) = substDefNormalInNeutral dv x nt
+
+substDefNormalInNeutral :: (LCNormalTerm, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
+substDefNormalInNeutral dv x = go
+  where
+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv
+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e
+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1
+    go (LCNeutApp f a) =
+      case go f of
+        LCNormLam _ b -> substituteNormalInNormal a' 0 b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substDefNormalInNormal dv x a
+
+shift :: (LCTerm, Int) -> LCTerm
+shift (v, s) = go 0 v
+  where
+    go n (LCVar x)   = LCVar $ if x < n then x else x + s
+    go n (LCLam t b) = LCLam t $ go (n + 1) b
+    go n (LCApp f a) = go n f `LCApp` go n a
+
+shiftType :: (LCType, Int) -> LCType
+shiftType = shiftTypeMin 0
+
+shiftTypeMin :: Int -> (LCType, Int) -> LCType
+shiftTypeMin m' (v, r) = go m' v
+  where
     go _ LCBase        = LCBase
-    go m e@(LCTVar l)  = if m == l then v else e
+    go m (LCTVar p)    = LCTVar $ if p < m then p else p + r
     go m (LCArr a b)   = go m a `LCArr` go m b
     go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
     go m (LCTTApp f a) = go m f `LCTTApp` go m a
 
-substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
-substituteValue n v = go n
-  where
-    go m e@(LCVar l) = if m == l then liftLCValue v else e
-    go m (LCLam t b) = LCLam t (go (m + 1) b)
-    go m (LCApp f a) = LCApp (go m f) (go m a)
+shiftValue :: (LCValue, Int) -> LCTerm
+shiftValue (v, s) = shift (liftLCValue v, s)
 
-substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormalInNormal n v = go n
+shiftNormal :: (LCNormalTerm, Int) -> LCNormalTerm
+shiftNormal = shiftNormalMin 0
+
+shiftNormalMin :: Int -> (LCNormalTerm, Int) -> LCNormalTerm
+shiftNormalMin n' (v, s) = go n' v
   where
-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
-    go m (LCNormNeut nt) = substituteNormalInNeutral m v nt
+    go n (LCNormLam t b) = LCNormLam t $ go (n + 1) b
+    go n (LCNormNeut nt) = LCNormNeut $ shiftNeutralMin n (nt, s)
 
-substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNormalInNeutral n v = go n
+shiftNeutralMin :: Int -> (LCNeutralTerm, Int) -> LCNeutralTerm
+shiftNeutralMin n (v, s) = go v
   where
-    go m e@(LCNeutVar l) = if m == l then v else LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b -> substituteNormalInNormal 0 a' b
-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
-      where
-        a' = substituteNormalInNormal m v a
+    go (LCNeutVar x)   = LCNeutVar $ if x < n then x else x + s
+    go (LCNeutApp f a) = go f `LCNeutApp` shiftNormalMin n (a, s)
diff --git a/src/LambdaCube/SystemFw_/TH.hs b/src/LambdaCube/SystemFw_/TH.hs
--- a/src/LambdaCube/SystemFw_/TH.hs
+++ b/src/LambdaCube/SystemFw_/TH.hs
@@ -1,49 +1,86 @@
 module LambdaCube.SystemFw_.TH
-  ( lc
+  ( qTerm
+  , qType
+  , qKind
   ) where
 
 import           Data.Data                   (Data)
 import           Data.Generics               (extQ)
-import           Data.Text                   (Text)
-import qualified Data.Text                   as Text
+import           LambdaCube.Common.TH
 import           LambdaCube.SystemFw_.Ast
 import           LambdaCube.SystemFw_.Parser
 import           Language.Haskell.TH.Lib     (ExpQ, varE)
 import           Language.Haskell.TH.Quote   (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax  (Loc (loc_start), dataToExpQ, lift,
-                                              location, mkName)
-import qualified Text.Megaparsec             as P
-import qualified Text.Megaparsec.Error       as PE
+import           Language.Haskell.TH.Syntax  (mkName)
 
-lc :: QuasiQuoter
-lc =
+qTerm :: QuasiQuoter
+qTerm =
   QuasiQuoter
-    { quoteExp = expLc
+    { quoteExp = qExpTerm
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-expLc :: String -> ExpQ
-expLc str = do
-  l <- location
-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> dataToExpQ converter e
-    Left err -> fail $ PE.errorBundlePretty err
+qExpTerm :: String -> ExpQ
+qExpTerm = qExpBase pTopTerm converter
   where
     converter :: Data b => b -> Maybe ExpQ
     converter =
-      const Nothing
+      converterBase
       `extQ` quotedMVar
       `extQ` quotedMTVar
       `extQ` quotedMKVar
-      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
     quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
     quotedMVar _             = Nothing
 
     quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
     quotedMTVar _              = Nothing
+
+    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
+    quotedMKVar _              = Nothing
+
+qType :: QuasiQuoter
+qType =
+  QuasiQuoter
+    { quoteExp = qExpType
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+qExpType :: String -> ExpQ
+qExpType = qExpBase pTopType converter
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      converterBase
+      `extQ` quotedMTVar
+      `extQ` quotedMKVar
+
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
+
+    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
+    quotedMKVar _              = Nothing
+
+qKind :: QuasiQuoter
+qKind =
+  QuasiQuoter
+    { quoteExp = qExpKind
+    , quotePat = undefined
+    , quoteType = undefined
+    , quoteDec = undefined
+    }
+
+qExpKind :: String -> ExpQ
+qExpKind = qExpBase pTopKind converter
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      converterBase
+      `extQ` quotedMKVar
 
     quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
     quotedMKVar _              = Nothing
diff --git a/src/LambdaCube/SystemFw_/TypeChecker.hs b/src/LambdaCube/SystemFw_/TypeChecker.hs
--- a/src/LambdaCube/SystemFw_/TypeChecker.hs
+++ b/src/LambdaCube/SystemFw_/TypeChecker.hs
@@ -1,5 +1,10 @@
-module LambdaCube.SystemFw_.TypeChecker where
+module LambdaCube.SystemFw_.TypeChecker
+  ( reduceType
 
+  , infer
+  , inferKind
+  ) where
+
 import           Data.List                         (uncons)
 import           LambdaCube.SystemFw_.Ast
 import           LambdaCube.SystemFw_.Substitution
@@ -14,7 +19,7 @@
     go (LCTTApp f a)
       | LCTTLam _ b <- go f
       , v <- go a
-      = go $ substituteTypeInType 0 v b
+      = go $ substituteTypeInType v 0 b
       | otherwise
       = error "Did you really kind check this?"
 
diff --git a/test/LambdaCube/STLCTest.hs b/test/LambdaCube/STLCTest.hs
new file mode 100644
--- /dev/null
+++ b/test/LambdaCube/STLCTest.hs
@@ -0,0 +1,168 @@
+{-# LANGUAGE QuasiQuotes #-}
+module LambdaCube.STLCTest
+  ( tests
+  ) where
+
+import qualified Control.Exception
+import           Control.Monad              (forM_, void)
+import qualified Data.Text                  as Text
+import           LambdaCube.STLC
+import           LambdaCube.STLCTestExample
+import           LambdaCube.TestUtil
+import           Test.Hspec
+import           Test.Tasty
+import           Test.Tasty.Hspec           (testSpec)
+
+newtype TestLCType = TestLCType LCType
+  deriving newtype (Eq)
+
+instance Show TestLCType where
+  show (TestLCType ty) = Text.unpack $ prettyUnnamedType ty
+
+newtype TestLCTerm = TestLCTerm LCTerm
+  deriving newtype (Eq)
+
+instance Show TestLCTerm where
+  show (TestLCTerm tm) = Text.unpack $ prettyUnnamedTerm tm
+
+tests :: IO TestTree
+tests = testSpec "STLC tests" spec
+
+spec :: Spec
+spec = do
+  describe "STLC infer" inferSpec
+  describe "STLC evaluate" evaluateSpec
+  describe "STLC normalize" normalizeSpec
+
+inferSpec :: SpecWith ()
+inferSpec = forM_ inferSpecCases $ \(mkTitle, extTm, extTy) -> do
+  let
+    tm = elaborate extTm
+    ty = elaborateType extTy
+  it (mkTitle tm ty) $ do
+    TestLCType (infer tm) `shouldBe` TestLCType ty
+
+inferSpecCases :: [(LCTerm -> LCType -> String, ExtLCTerm, ExtLCType)]
+inferSpecCases =
+  [ ( const2 "infer lcBaseId should be lcBaseArr"
+    , lcBaseId
+    , lcBaseArr
+    )
+  , ( makeDefaultInferTitle
+    , [qTerm| \x : # . $lcBaseArrId $lcBaseId x |]
+    , lcBaseArr
+    )
+  , ( makeDefaultInferTitle
+    , [qTerm| \x : $lcBaseArr . \y : $lcBaseArr . \z : # . x (y z) |]
+    , [qType| $lcBaseArr -> $lcBaseArr -> $lcBaseArr |]
+    )
+  , ( makeDefaultInferTitle
+    , [qTerm| \abc : # . (\fdd : $lcBaseArr . fdd abc) |]
+    , [qType| # -> $lcBaseArr -> # |]
+    )
+  , ( const2 "infer pcn3 should be pcnTy"
+    , lcPCN3
+    , lcPCNTy
+    )
+  , ( const2 "infer lcPCNAdd should be (lcPCNTy -> lcPCNTy -> lcPCNTy)"
+    , lcPCNAdd
+    , [qType| $lcPCNTy -> $lcPCNTy -> $lcPCNTy |]
+    )
+  , ( const2 "infer (lcPCNAdd lcPCN1 lcPCN2) should be lcPCNTy"
+    , [qTerm| $lcPCNAdd $lcPCN1 $lcPCN2 |]
+    , [qType| $lcPCNTy |]
+    )
+  , ( const2 "infer lcPCNMul should be (lcPCNTy -> lcPCNTy -> lcPCNTy)"
+    , lcPCNMul
+    , [qType| $lcPCNTy -> $lcPCNTy -> $lcPCNTy |]
+    )
+  , ( const2 "infer (lcPCNMul lcPCN0) should be (lcPCNTy -> lcPCNTy)"
+    , [qTerm| $lcPCNMul $lcPCN0 |]
+    , [qType| $lcPCNTy -> $lcPCNTy |]
+    )
+  ]
+
+evaluateSpec :: SpecWith ()
+evaluateSpec = forM_ evaluateSpecCases $ \(mkTitle, extTm, extResTm) -> do
+  let
+    tm = elaborate extTm
+    resTm = elaborate extResTm
+  it (mkTitle tm resTm) $ do
+    void . Control.Exception.evaluate $ infer tm
+    void . Control.Exception.evaluate $ infer resTm
+    TestLCTerm (liftLCValue (evaluate tm)) `shouldBe` TestLCTerm (liftLCValue (evaluate resTm))
+
+evaluateSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]
+evaluateSpecCases =
+  [ ( makeDefaultEvaluateTitle
+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]
+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]
+    )
+  , ( const2 "evaluate (lcBaseArrId lcBaseId) should be lcBaseId"
+    , [qTerm| $lcBaseArrId $lcBaseId |]
+    , lcBaseId
+    )
+  , ( const2 "evaluate (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"
+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]
+    , lcBaseId
+    )
+  , ( const2 "evaluate (lcPCNAdd lcPCN1 lcPCN2) should be lcPCN3 with unnormalized parts"
+    , [qTerm| $lcPCNAdd $lcPCN1 $lcPCN2 |]
+    , [qTerm| \s : $lcBaseArr . \z : # . $lcPCN1 s ($lcPCN2 s z) |]
+    )
+  ]
+
+normalizeSpec :: SpecWith ()
+normalizeSpec = forM_ normalizeSpecCases $ \(mkTitle, extTm, extResTm) -> do
+  let
+    tm = elaborate extTm
+    resTm = elaborate extResTm
+  it (mkTitle tm resTm) $ do
+    void . Control.Exception.evaluate $ infer tm
+    void . Control.Exception.evaluate $ infer resTm
+    TestLCTerm (liftLCNormal (normalize tm)) `shouldBe` TestLCTerm (liftLCNormal (normalize resTm))
+
+normalizeSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]
+normalizeSpecCases =
+  [ ( makeDefaultNormalizeTitle
+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]
+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]
+    )
+  , ( const2 "normalize (lcBaseArrId lcBaseId) should be lcBaseId"
+    , [qTerm| $lcBaseArrId $lcBaseId |]
+    , lcBaseId
+    )
+  , ( const2 "normalize (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"
+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]
+    , lcBaseId
+    )
+  , ( const2 "normalize (lcPCNAdd lcPCN1 lcPCN2) should be lcPCN3"
+    , [qTerm| $lcPCNAdd $lcPCN0 $lcPCN1 |]
+    , lcPCN1
+    )
+  , ( const2 "normalize (lcPCN4 lcBaseId) should be lcBaseId"
+    , [qTerm| $lcPCN4 $lcBaseId |]
+    , lcBaseId
+    )
+  ]
+
+makeDefaultInferTitle :: LCTerm -> LCType -> String
+makeDefaultInferTitle tm ty =
+  makeDefaultTitle
+  "infer"
+  (prettyShowUnnamedTerm tm)
+  (prettyShowUnnamedType ty)
+
+makeDefaultEvaluateTitle :: LCTerm -> LCTerm -> String
+makeDefaultEvaluateTitle tm resTm =
+  makeDefaultTitle
+  "evaluate"
+  (prettyShowUnnamedTerm tm)
+  (prettyShowUnnamedTerm resTm)
+
+makeDefaultNormalizeTitle :: LCTerm -> LCTerm -> String
+makeDefaultNormalizeTitle tm resTm =
+  makeDefaultTitle
+  "normalize"
+  (prettyShowUnnamedTerm tm)
+  (prettyShowUnnamedTerm resTm)
diff --git a/test/LambdaCube/STLCTestExample.hs b/test/LambdaCube/STLCTestExample.hs
new file mode 100644
--- /dev/null
+++ b/test/LambdaCube/STLCTestExample.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE QuasiQuotes #-}
+module LambdaCube.STLCTestExample where
+
+import           LambdaCube.STLC
+
+lcBaseId, lcBaseArrId :: ExtLCTerm
+lcBaseId = [qTerm| \x : # . x |]
+lcBaseArrId = [qTerm| \x : $lcBaseArr . x |]
+
+lcBaseArr :: ExtLCType
+lcBaseArr = [qType| # -> # |]
+
+------------------------------------------------------------
+-- Pseudo Church Numeral examples
+------------------------------------------------------------
+
+lcPCN0, lcPCN1, lcPCN2, lcPCN3, lcPCN4, lcPCN5 :: ExtLCTerm
+lcPCN0 = [qTerm| \s : $lcBaseArr . $lcBaseId |]
+lcPCN1 = [qTerm| \s : $lcBaseArr . \z : # . s z |]
+lcPCN2 = [qTerm| \s : $lcBaseArr . \z : # . s (s z) |]
+lcPCN3 = [qTerm| \s : $lcBaseArr . \z : # . s (s (s z)) |]
+lcPCN4 = [qTerm| \s : $lcBaseArr . \z : # . s (s (s (s z))) |]
+lcPCN5 = [qTerm| \s : $lcBaseArr . \z : # . s (s (s (s (s z)))) |]
+
+lcPCNAdd, lcPCNMul :: ExtLCTerm
+lcPCNAdd =
+  [qTerm|
+     \n : $lcPCNTy . \m : $lcPCNTy .
+     \s : $lcBaseArr . \z : # . n s (m s z)
+  |]
+lcPCNMul =
+  [qTerm|
+     \n : $lcPCNTy . \m : $lcPCNTy .
+     \s : $lcBaseArr . \z : # . n (m s) z
+  |]
+
+lcPCNTy :: ExtLCType
+lcPCNTy = [qType| $lcBaseArr -> $lcBaseArr |]
diff --git a/test/LambdaCube/SystemFwTest.hs b/test/LambdaCube/SystemFwTest.hs
new file mode 100644
--- /dev/null
+++ b/test/LambdaCube/SystemFwTest.hs
@@ -0,0 +1,282 @@
+{-# LANGUAGE QuasiQuotes #-}
+module LambdaCube.SystemFwTest where
+
+import qualified Control.Exception
+import           Control.Monad                  (forM_, void)
+import qualified Data.Text                      as Text
+import           LambdaCube.SystemFw
+import           LambdaCube.SystemFwTestExample
+import           LambdaCube.TestUtil
+import           Test.Hspec
+import           Test.Tasty
+import           Test.Tasty.Hspec               (testSpec)
+
+newtype TestLCType = TestLCType LCType
+  deriving newtype (Eq)
+
+instance Show TestLCType where
+  show (TestLCType ty) = Text.unpack $ prettyUnnamedType ty
+
+newtype TestLCTerm = TestLCTerm LCTerm
+  deriving newtype (Eq)
+
+instance Show TestLCTerm where
+  show (TestLCTerm tm) = Text.unpack $ prettyUnnamedTerm tm
+
+tests :: IO TestTree
+tests = testSpec "SystemFw tests" spec
+
+spec :: Spec
+spec = do
+  describe "SystemFw infer" inferSpec
+  describe "SystemFw evaluate" evaluateSpec
+  describe "SystemFw normalize" normalizeSpec
+
+inferSpec :: SpecWith ()
+inferSpec = forM_ inferSpecCases $ \(mkTitle, extTm, extTy) -> do
+  let
+    tm = elaborate extTm
+    ty = elaborateType [] extTy
+  it (mkTitle tm ty) $ do
+    TestLCType (infer tm) `shouldBe` TestLCType (reduceType ty)
+
+inferSpecCases :: [(LCTerm -> LCType -> String, ExtLCTerm, ExtLCType)]
+inferSpecCases =
+  [ ( const2 "infer lcBaseId should be lcBaseArr"
+    , lcBaseId
+    , lcBaseArr
+    )
+  , ( makeDefaultInferTitle
+    , [qTerm| \x : # . $lcBaseArrId $lcBaseId x |]
+    , lcBaseArr
+    )
+  , ( makeDefaultInferTitle
+    , [qTerm| \x : $lcBaseArr . \y : $lcBaseArr . \z : # . x (y z) |]
+    , [qType| $lcBaseArr -> $lcBaseArr -> $lcBaseArr |]
+    )
+  , ( makeDefaultInferTitle
+    , [qTerm| \abc : # . (\fdd : $lcBaseArr . fdd abc) |]
+    , [qType| # -> $lcBaseArr -> # |]
+    )
+  , ( const2 "infer lcId should be (! a : * , a -> a)"
+    , lcId
+    , [qType| ! a : * , a -> a |]
+    )
+  , ( const2 "infer pCN3 should be pCNTy"
+    , lcCN3
+    , lcCNTy
+    )
+  , ( const2 "infer lcCNSucc should be (lcCNTy -> lcCNTy)"
+    , [qTerm| $lcCNSucc |]
+    , [qType| $lcCNTy -> $lcCNTy |]
+    )
+  , ( const2 "infer lcCNAdd should be (lcCNTy -> lcCNTy -> lcCNTy)"
+    , lcCNAdd
+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]
+    )
+  , ( const2 "infer (lcCNAdd lcCN1 lcCN2) should be lcCNTy"
+    , [qTerm| $lcCNAdd $lcCN1 $lcCN2 |]
+    , [qType| $lcCNTy |]
+    )
+  , ( const2 "infer lcCNMul should be (lcCNTy -> lcCNTy -> lcCNTy)"
+    , lcCNMul
+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]
+    )
+  , ( const2 "infer (lcCNMul lcCN0) should be (lcCNTy -> lcCNTy)"
+    , [qTerm| $lcCNMul $lcCN0 |]
+    , [qType| $lcCNTy -> $lcCNTy |]
+    )
+  , ( const2 "infer lcCNPred should be (lcCNTy -> lcCNTy)"
+    , [qTerm| $lcCNPred |]
+    , [qType| $lcCNTy -> $lcCNTy |]
+    )
+  , ( const2 "infer lcCNPredDef should be (lcCNTy -> lcCNTy -> lcCNTy)"
+    , [qTerm| $lcCNPredDef |]
+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]
+    )
+  , ( const2 "infer lcCNMinus should be (lcCNTy -> lcCNTy -> lcCNTy)"
+    , [qTerm| $lcCNMinus |]
+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]
+    )
+  , ( const2 "infer lcCNIs0 should be (lcCNTy -> lcCBTy)"
+    , [qTerm| $lcCNIs0 |]
+    , [qType| $lcCNTy -> $lcCBTy |]
+    )
+  , ( const2 "infer lcCLNil should be (!e : * , lcCLTy e)"
+    , [qTerm| $lcCLNil |]
+    , [qType| !e : * , $lcCLTy e |]
+    )
+  , ( const2 "infer lcCLCons should be (!e : * , e -> lcCLTy e -> lcCLTy e)"
+    , [qTerm| $lcCLCons |]
+    , [qType| !e : * , e -> $lcCLTy e -> $lcCLTy e |]
+    )
+  , ( const2 "infer lcCL_CN_0_1_2 should be (lcCLTy lcCNTy)"
+    , [qTerm| $lcCL_CN_0_1_2 |]
+    , [qType| $lcCLTy $lcCNTy |]
+    )
+  , ( const2 "infer lcCLHeadDef should be (!e : * , e -> lcCLTy e -> e)"
+    , [qTerm| $lcCLHeadDef |]
+    , [qType| !e : * , e -> $lcCLTy e -> e |]
+    )
+  , ( const2 "infer lcCLTail should be (!e : * , lcCLTy e -> lcCLTy e)"
+    , [qTerm| $lcCLTail |]
+    , [qType| !e : * , $lcCLTy e -> $lcCLTy e |]
+    )
+  , ( const2 "infer lcCLTailDef should be (!e : * , lcCLTy e -> lcCLTy e -> lcCLTy e)"
+    , [qTerm| $lcCLTailDef |]
+    , [qType| !e : * , $lcCLTy e -> $lcCLTy e -> $lcCLTy e |]
+    )
+  ]
+
+evaluateSpec :: SpecWith ()
+evaluateSpec = forM_ evaluateSpecCases $ \(mkTitle, extTm, extResTm) -> do
+  let
+    tm = elaborate extTm
+    resTm = elaborate extResTm
+  it (mkTitle tm resTm) $ do
+    void . Control.Exception.evaluate $ infer tm
+    void . Control.Exception.evaluate $ infer resTm
+    TestLCTerm (liftLCValue (evaluate tm)) `shouldBe` TestLCTerm (liftLCValue (evaluate resTm))
+
+evaluateSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]
+evaluateSpecCases =
+  [ ( makeDefaultEvaluateTitle
+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]
+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]
+    )
+  , ( const2 "evaluate (lcBaseArrId lcBaseId) should be lcBaseId"
+    , [qTerm| $lcBaseArrId $lcBaseId |]
+    , lcBaseId
+    )
+  , ( const2 "evaluate (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"
+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]
+    , lcBaseId
+    )
+  , ( const2 "evaluate (lcCNAdd lcCN1 lcCN2) should be lcCN3 with unnormalized parts"
+    , [qTerm| $lcCNAdd $lcCN1 $lcCN2 |]
+    , [qTerm| @\r : * . \s : r -> r . \z : r . $lcCN1 @r s ($lcCN2 @r s z) |]
+    )
+  , ( const2 "evaluate (lcCNSucc lcCN1) should be lcCN2 with unnormalized parts"
+    , [qTerm| $lcCNSucc $lcCN1 |]
+    , [qTerm| @\r : * . \s : r -> r . \z : r . s ($lcCN1 @r s z) |]
+    )
+  , ( const2 "evaluate (lcCNPredDef lcCN5 lcCN1) should be lcCN0"
+    , [qTerm| $lcCNPredDef $lcCN5 $lcCN1 |]
+    , [qTerm| $lcCN0 |]
+    )
+  , ( const2 "evaluate (lcCNPredDef lcCN5 lcCN0) should be lcCN5"
+    , [qTerm| $lcCNPredDef $lcCN5 $lcCN0 |]
+    , [qTerm| $lcCN5 |]
+    )
+  , ( const2 "evaluate (lcCNIs0 lcCN0) should be lcCBTrue"
+    , [qTerm| $lcCNIs0 $lcCN0 |]
+    , [qTerm| $lcCBTrue |]
+    )
+  , ( const2 "evaluate (lcCNIs0 lcCN2) should be lcCBFalse"
+    , [qTerm| $lcCNIs0 $lcCN2 |]
+    , [qTerm| $lcCBFalse |]
+    )
+  , ( const2 "evaluate (lcCLHeadDef @lcCNTy lcCN3 lcCL_CN_0_1_2) should be lcCN0"
+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 $lcCL_CN_0_1_2 |]
+    , [qTerm| $lcCN0 |]
+    )
+  , ( const2 "evaluate (lcCLTailDef lcCL_CN_0_1_2 (lcCLTailDef lcCL_CN_0_1_2 lcCL_CN_0)) should be lcCL_CN_0_1_2"
+    , [qTerm| $lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 ($lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 $lcCL_CN_0) |]
+    , [qTerm| $lcCL_CN_0_1_2 |]
+    )
+  ]
+
+normalizeSpec :: SpecWith ()
+normalizeSpec = forM_ normalizeSpecCases $ \(mkTitle, extTm, extResTm) -> do
+  let
+    tm = elaborate extTm
+    resTm = elaborate extResTm
+  it (mkTitle tm resTm) $ do
+    void . Control.Exception.evaluate $ infer tm
+    void . Control.Exception.evaluate $ infer resTm
+    TestLCTerm (liftLCNormal (normalize tm)) `shouldBe` TestLCTerm (liftLCNormal (normalize resTm))
+
+normalizeSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]
+normalizeSpecCases =
+  [ ( makeDefaultNormalizeTitle
+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]
+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]
+    )
+  , ( const2 "normalize (lcBaseArrId lcBaseId) should be lcBaseId"
+    , [qTerm| $lcBaseArrId $lcBaseId |]
+    , lcBaseId
+    )
+  , ( const2 "normalize (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"
+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]
+    , lcBaseId
+    )
+  , ( const2 "normalize (lcCNAdd lcCN1 lcCN2) should be lcCN3"
+    , [qTerm| $lcCNAdd $lcCN0 $lcCN1 |]
+    , lcCN1
+    )
+  , ( const2 "normalize (lcCN4 lcBaseId) should be lcBaseId"
+    , [qTerm| $lcCN4 @# $lcBaseId |]
+    , lcBaseId
+    )
+  , ( const2 "normalize (lcCNPred lcCN4) should be lcCN3"
+    , [qTerm| $lcCNPred $lcCN4 |]
+    , lcCN3
+    )
+  , ( const2 "normalize (lcCNMinus lcCN5 lcCN3) should be lcCN2"
+    , [qTerm| $lcCNMinus $lcCN5 $lcCN3 |]
+    , lcCN2
+    )
+  , ( const2 "normalize (lcCNIs0 lcCN0) should be lcCBTrue"
+    , [qTerm| $lcCNIs0 $lcCN0 |]
+    , [qTerm| $lcCBTrue |]
+    )
+  , ( const2 "normalize (lcCNIs0 lcCN2) should be lcCBFalse"
+    , [qTerm| $lcCNIs0 $lcCN2 |]
+    , [qTerm| $lcCBFalse |]
+    )
+  , ( const2 "normalize (lcCLHeadDef lcCN3 lcCL_CN_0_1_2) should be lcCN0"
+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 $lcCL_CN_0_1_2 |]
+    , [qTerm| $lcCN0 |]
+    )
+  , ( const2 "normalize (lcCLHeadDef lcCN3 (lcCLTail lcCL_CN_0_1_2)) should be lcCN1"
+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 ($lcCLTail @$lcCNTy $lcCL_CN_0_1_2) |]
+    , [qTerm| $lcCN1 |]
+    )
+  , ( const2 "normalize (lcCLHeadDef lcCN3 (lcCLTail (lcCLTail lcCL_CN_0_1_2))) should be lcCN2"
+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 ($lcCLTail @$lcCNTy ($lcCLTail @$lcCNTy $lcCL_CN_0_1_2)) |]
+    , [qTerm| $lcCN2 |]
+    )
+  , ( const2 "normalize (lcCLTail (lcCLTail (lcCLTail lcCL_CN_0_1_2))) should be lcCLNil"
+    , [qTerm| $lcCLTail @$lcCNTy ($lcCLTail @$lcCNTy ($lcCLTail @$lcCNTy $lcCL_CN_0_1_2)) |]
+    , [qTerm| $lcCLNil @$lcCNTy |]
+    )
+  , ( const2 "normalize (lcCLTailDef lcCL_CN_0_1_2 lcCL_CN_0) should be lcCLNil"
+    , [qTerm| $lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 $lcCL_CN_0 |]
+    , [qTerm| $lcCLNil @$lcCNTy |]
+    )
+  , ( const2 "normalize (lcCLTailDef lcCL_CN_0_1_2 (lcCLTailDef lcCL_CN_0_1_2 lcCL_CN_0)) should be lcCL_CN_0_1_2"
+    , [qTerm| $lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 ($lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 $lcCL_CN_0) |]
+    , [qTerm| $lcCL_CN_0_1_2 |]
+    )
+  ]
+
+makeDefaultInferTitle :: LCTerm -> LCType -> String
+makeDefaultInferTitle tm ty =
+  makeDefaultTitle
+  "infer"
+  (prettyShowUnnamedTerm tm)
+  (prettyShowUnnamedType ty)
+
+makeDefaultEvaluateTitle :: LCTerm -> LCTerm -> String
+makeDefaultEvaluateTitle tm resTm =
+  makeDefaultTitle
+  "evaluate"
+  (prettyShowUnnamedTerm tm)
+  (prettyShowUnnamedTerm resTm)
+
+makeDefaultNormalizeTitle :: LCTerm -> LCTerm -> String
+makeDefaultNormalizeTitle tm resTm =
+  makeDefaultTitle
+  "normalize"
+  (prettyShowUnnamedTerm tm)
+  (prettyShowUnnamedTerm resTm)
diff --git a/test/LambdaCube/SystemFwTestExample.hs b/test/LambdaCube/SystemFwTestExample.hs
new file mode 100644
--- /dev/null
+++ b/test/LambdaCube/SystemFwTestExample.hs
@@ -0,0 +1,184 @@
+{-# LANGUAGE QuasiQuotes #-}
+module LambdaCube.SystemFwTestExample where
+
+import           LambdaCube.SystemFw
+
+lcBaseId, lcBaseArrId :: ExtLCTerm
+lcBaseId = [qTerm| \x : # . x |]
+lcBaseArrId = [qTerm| \x : $lcBaseArr . x |]
+
+lcBaseArr :: ExtLCType
+lcBaseArr = [qType| # -> # |]
+
+lcId :: ExtLCTerm
+lcId = [qTerm| @\a : * . \x : a . x |]
+
+------------------------------------------------------------
+-- Church Pair examples
+------------------------------------------------------------
+
+lcCPPair :: ExtLCTerm
+lcCPPair = [qTerm| @\a : * . @\b : * . \x : a . \y : b . @\r : * . \f : a -> b -> r . f x y |]
+
+lcCPFst :: ExtLCTerm
+lcCPFst = [qTerm| @\a : * . @\b : * . \p : $lcCPTy a b . p @a (\x : a . \y : b . x) |]
+
+lcCPSnd :: ExtLCTerm
+lcCPSnd = [qTerm| @\a : * . @\b : * . \p : $lcCPTy a b . p @b (\x : a . \y : b . y) |]
+
+lcCPTy :: ExtLCType
+lcCPTy = [qType| \a : * . \b : * . !r : * , (a -> b -> r) -> r |]
+
+------------------------------------------------------------
+-- Church Boolean examples
+------------------------------------------------------------
+
+lcCBTrue, lcCBFalse :: ExtLCTerm
+lcCBTrue = [qTerm| @\r : * . \t : r . \f : r . t |]
+lcCBFalse = [qTerm| @\r : * . \t : r . \f : r . f |]
+
+lcCBIf :: ExtLCTerm
+lcCBIf = [qTerm| \b : $lcCBTy . b |]
+
+lcCBAnd, lcCBOr :: ExtLCTerm
+lcCBAnd = [qTerm| \b1 : $lcCBTy . \b2 : $lcCBTy . @\r : * . \t : r . \f : r . b1 @r (b2 @r t f) f |]
+lcCBOr = [qTerm| \b1 : $lcCBTy . \b2 : $lcCBTy . @\r : * . \t : r . \f : r . b1 @r t (b2 @r t f) |]
+
+lcCBNot :: ExtLCTerm
+lcCBNot = [qTerm| \b : $lcCBTy . @\r : * . \t : r . \f : r . b @r f t |]
+
+lcCBTy :: ExtLCType
+lcCBTy = [qType| !r : * , r -> r -> r |]
+
+------------------------------------------------------------
+-- Church Numeral examples
+------------------------------------------------------------
+
+lcCN1, lcCN2, lcCN3, lcCN4, lcCN5 :: ExtLCTerm
+lcCN1 = [qTerm| @\r : * . \s : r -> r . \z : r . s z |]
+lcCN2 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s z) |]
+lcCN3 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s (s z)) |]
+lcCN4 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s (s (s z))) |]
+lcCN5 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s (s (s (s z)))) |]
+
+lcCN0, lcCNSucc :: ExtLCTerm
+lcCN0 = [qTerm| @\r : * . \s : r -> r . \z : r . z |]
+lcCNSucc = [qTerm| \n : $lcCNTy . @\r : * . \s : r -> r . \z : r . s (n @r s z) |]
+
+lcCNPred, lcCNPredDef :: ExtLCTerm
+lcCNPred =
+  [qTerm|
+     \n : $lcCNTy .
+     @\r : * . \s : r -> r . \z : r .
+     n
+     @((r -> r) -> r)
+     (\p : (r -> r) -> r . \g : r -> r . g (p s))
+     (\p : r -> r . z)
+     (\p : r . p)
+  |]
+lcCNPredDef =
+  [qTerm|
+     \d : $lcCNTy .
+     \n : $lcCNTy .
+     n
+     @(($lcCNTy -> $lcCNTy -> $lcCNTy) -> $lcCNTy)
+     (\p : ($lcCNTy -> $lcCNTy -> $lcCNTy) -> $lcCNTy .
+      \g : $lcCNTy -> $lcCNTy -> $lcCNTy .
+      (\x : $lcCNTy . g ($lcCNSucc x) x) (p (\x : $lcCNTy . \y : $lcCNTy . x)))
+     (\g : $lcCNTy -> $lcCNTy -> $lcCNTy . g $lcCN0 d)
+     (\x : $lcCNTy . \y : $lcCNTy . y)
+  |]
+
+lcCNAdd, lcCNMul, lcCNMinus :: ExtLCTerm
+lcCNAdd =
+  [qTerm|
+     \n : $lcCNTy . \m : $lcCNTy .
+     @\r : * . \s : r -> r . \z : r . n @r s (m @r s z)
+  |]
+lcCNMul =
+  [qTerm|
+     \n : $lcCNTy . \m : $lcCNTy .
+     @\r : * . \s : r -> r . \z : r . n @r (m @r s) z
+  |]
+lcCNMinus =
+  [qTerm|
+     \n : $lcCNTy . \m : $lcCNTy . m @$lcCNTy $lcCNPred n
+  |]
+
+lcCNIs0 :: ExtLCTerm
+lcCNIs0 =
+  [qTerm|
+     \n : $lcCNTy . n @$lcCBTy (\x : $lcCBTy . $lcCBFalse) $lcCBTrue
+  |]
+
+lcCNTy :: ExtLCType
+lcCNTy = [qType| !r : * , (r -> r) -> r -> r |]
+
+------------------------------------------------------------
+-- Church List examples
+------------------------------------------------------------
+
+lcCL_CN_0, lcCL_CN_0_1, lcCL_CN_0_1_2 :: ExtLCTerm
+lcCL_CN_0 =
+  [qTerm|
+    $lcCLCons @$lcCNTy $lcCN0
+    ($lcCLNil @$lcCNTy)
+  |]
+lcCL_CN_0_1 =
+  [qTerm|
+    $lcCLCons @$lcCNTy $lcCN0
+    ($lcCLCons @$lcCNTy $lcCN1
+    ($lcCLNil @$lcCNTy))
+  |]
+lcCL_CN_0_1_2 =
+  [qTerm|
+    $lcCLCons @$lcCNTy $lcCN0
+    ($lcCLCons @$lcCNTy $lcCN1
+    ($lcCLCons @$lcCNTy $lcCN2
+    ($lcCLNil @$lcCNTy)))
+  |]
+
+lcCLNil, lcCLCons :: ExtLCTerm
+lcCLNil = [qTerm| @\e : * . @\r : * . \c : e -> r -> r . \n : r . n |]
+lcCLCons =
+  [qTerm|
+    @\e : * .
+    \h : e . \t : $lcCLTy e .
+    @\r : * . \c : e -> r -> r . \n : r . c h (t @r c n)
+  |]
+
+lcCLLength :: ExtLCTerm
+lcCLLength = [qTerm| @\e : * . \l : $lcCLTy e . l @$lcCNTy (\h : e . \t : $lcCNTy . $lcCNSucc t) $lcCN0 |]
+
+lcCLHeadDef :: ExtLCTerm
+lcCLHeadDef = [qTerm| @\e : * . \d : e . \l : $lcCLTy e . l @e (\h : e . \t : e . h) d |]
+
+lcCLTail, lcCLTailDef :: ExtLCTerm
+lcCLTail =
+  [qTerm|
+    @\e : * .
+    \l : $lcCLTy e .
+    @\r : * . \c : e -> r -> r . \n : r .
+    l
+    @((e -> r -> r) -> r)
+    (\h : e . \t : (e -> r -> r) -> r . \g : e -> r -> r . g h (t c))
+    (\t : e -> r -> r . n)
+    (\h : e . \t : r . t)
+  |]
+lcCLTailDef =
+  [qTerm|
+    @\e : * .
+    \d : $lcCLTy e .
+    \l : $lcCLTy e .
+    l
+    @(($lcCLTy e -> $lcCLTy e -> $lcCLTy e) -> $lcCLTy e)
+    (\h : e .
+     \t : ($lcCLTy e -> $lcCLTy e -> $lcCLTy e) -> $lcCLTy e .
+     \g : $lcCLTy e -> $lcCLTy e -> $lcCLTy e .
+     (\x : $lcCLTy e . g ($lcCLCons @e h x) x) (t (\x : $lcCLTy e . \y : $lcCLTy e . x)))
+    (\g : $lcCLTy e -> $lcCLTy e -> $lcCLTy e . g ($lcCLNil @e) d)
+    (\x : $lcCLTy e . \y : $lcCLTy e . y)
+  |]
+
+lcCLTy :: ExtLCType
+lcCLTy = [qType| \e : * . !r : * , (e -> r -> r) -> r -> r |]
diff --git a/test/LambdaCube/TestUtil.hs b/test/LambdaCube/TestUtil.hs
new file mode 100644
--- /dev/null
+++ b/test/LambdaCube/TestUtil.hs
@@ -0,0 +1,15 @@
+module LambdaCube.TestUtil where
+
+const2 :: a -> b -> c -> a
+const2 x _ _ = x
+
+makeDefaultTitle :: String -> String -> String -> String
+makeDefaultTitle fName left right =
+  concat
+  [ fName
+  , " ("
+  , left
+  , ") should be ("
+  , right
+  , ")"
+  ]
diff --git a/test/Spec.hs b/test/Spec.hs
deleted file mode 100644
--- a/test/Spec.hs
+++ /dev/null
@@ -1,1 +0,0 @@
-{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
diff --git a/test/Test.hs b/test/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Test.hs
@@ -0,0 +1,16 @@
+module Main
+  ( main
+  ) where
+
+import qualified LambdaCube.STLCTest     as STLC
+import qualified LambdaCube.SystemFwTest as SystemFw
+import           Test.Tasty
+
+main :: IO ()
+main = do
+  testsForSTLC <- STLC.tests
+  testsForSystemFw <- SystemFw.tests
+  defaultMain $ testGroup "tests"
+    [ testsForSTLC
+    , testsForSystemFw
+    ]