diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+# 0.0.2
+
+- Add `LiftedModule` allowing to lift into 'ScopeH'.
+
 # 0.0.1
 
 - Relax 
diff --git a/bound-extras.cabal b/bound-extras.cabal
--- a/bound-extras.cabal
+++ b/bound-extras.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.2
 name:               bound-extras
-version:            0.0.1
+version:            0.0.2
 synopsis:           ScopeH and ScopeT extras for bound
 category:           Language, Compilers, Interpreters
 description:
@@ -27,9 +27,13 @@
 maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi>
 homepage:           https://github.com/phadej/bound-extras
 bug-reports:        https://github.com/phadej/bound-extras/issues
-tested-with:        GHC ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1
-extra-source-files: CHANGELOG.md examples/*.txt
+tested-with:
+  GHC ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.4 || ==8.10.4 || ==9.0.1 || ==9.2.1
 
+extra-source-files:
+  CHANGELOG.md
+  examples/*.txt
+
 source-repository head
   type:     git
   location: https://github.com/phadej/bound-extras
@@ -45,14 +49,13 @@
 
   -- GHC boot libraries
   build-depends:
-    , base          ^>=4.9.1.0 || ^>=4.10.1.0 || ^>=4.11.1.0 || ^>=4.12.0.0
+    , base          ^>=4.9.1.0 || ^>=4.10.1.0 || ^>=4.11.1.0 || ^>=4.12.0.0 || ^>=4.13.0.0 || ^>=4.14.0.0 || ^>=4.15.0.0 || ^>=4.16.0.0
     , deepseq       ^>=1.4.2.0
-    , hashable      ^>=1.2.7.0
+    , hashable      ^>=1.2.7.0 || ^>=1.3.0.0 || ^>=1.4.0.1
     , transformers  ^>=0.5.0.0
 
   -- other deps
-  build-depends:
-    , bound         ^>=2.0.1
+  build-depends:    bound ^>=2.0.1
 
   if !impl(ghc >=8.2)
     build-depends: bifunctors ^>=5.5.3
@@ -61,7 +64,10 @@
   type:             exitcode-stdio-1.0
   main-is:          Examples.hs
   other-modules:
+    Adjunctions
     BiSTLC
+    BiSTLC2
+    BiSTLC3
     Pretty
     SystemF
 
@@ -69,13 +75,14 @@
   hs-source-dirs:   examples
   ghc-options:      -Wall
   build-depends:
+    , adjunctions   ^>=4.4
     , base
     , bound
     , bound-extras
     , containers    ^>=0.5.7.1 || ^>=0.6.0.1
     , filepath      ^>=1.4.1.1
     , pretty        ^>=1.1.3.3
-    , tasty         >=1.1.0.3 && <1.3
+    , tasty         >=1.1.0.3 && <1.5
     , tasty-golden  ^>=2.3.2
     , text-short    ^>=0.1.2
     , transformers  ^>=0.5.0.0
diff --git a/examples/Adjunctions.hs b/examples/Adjunctions.hs
new file mode 100644
--- /dev/null
+++ b/examples/Adjunctions.hs
@@ -0,0 +1,13 @@
+module Adjunctions where
+
+import Data.Functor.Adjunction (Adjunction (..))
+
+-- Defining 'mjoin' for monad arising from adjunction is easy:
+-- every @r f@ is right module of @u f@.
+mjoinAdj :: (Functor r, Adjunction f u) => r (f (u (f a))) -> r (f a)
+mjoinAdj = fmap counit
+
+-- However 'LiftedModule' is trickier, here we need 
+-- to know more.
+mliftAdj :: (Functor r, Adjunction f u) => u (f a) -> r (f a)
+mliftAdj = error "we need to know about r, f and u"
diff --git a/examples/BiSTLC.hs b/examples/BiSTLC.hs
--- a/examples/BiSTLC.hs
+++ b/examples/BiSTLC.hs
@@ -100,6 +100,9 @@
     If c t e      >>== k = If (c >>== k) (t >>== k) (e >>== k)
     FoldNat z s n >>== k = FoldNat (z >>== k) (s >>== k) (n >>== k)
 
+instance LiftedModule Chk Inf where
+    mlift = Inf
+
 lam_ :: Eq a => a -> Chk a -> Chk a
 lam_ x b = Lam (abstract1H x b)
 
diff --git a/examples/BiSTLC2.hs b/examples/BiSTLC2.hs
new file mode 100644
--- /dev/null
+++ b/examples/BiSTLC2.hs
@@ -0,0 +1,417 @@
+{-# LANGUAGE DeriveFoldable         #-}
+{-# LANGUAGE DeriveFunctor          #-}
+{-# LANGUAGE DeriveTraversable      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE OverloadedStrings      #-}
+module BiSTLC2 (tests) where
+
+import Bound.ScopeH
+import Bound.Var            (Var (..), unvar)
+import Control.Monad        (ap)
+import Control.Monad.Module
+import Data.Bifunctor       (first)
+import Data.String          (IsString (..))
+import Data.Void            (Void)
+import System.FilePath      ((-<.>), (</>))
+import Test.Tasty           (TestTree, testGroup)
+import Test.Tasty.Golden    (goldenVsString)
+
+import qualified Data.ByteString.Lazy.UTF8 as UTF8
+import qualified Data.Text.Short           as TS
+
+import Pretty
+
+-------------------------------------------------------------------------------
+-- Types
+-------------------------------------------------------------------------------
+
+-- | Types.
+data Ty
+    = Ty ShortText
+    | TUnit
+    | Ty :+: Ty
+    | Ty :*: Ty
+    | Ty :-> Ty
+  deriving Eq
+
+infixr 2 :->
+infix 4 :*:
+infix 3 :+:
+
+instance IsString Ty where
+    fromString = Ty . fromString
+
+-------------------------------------------------------------------------------
+-- Infession
+-------------------------------------------------------------------------------
+
+-- | Inferable terms
+data Inf ty a
+    -- Variable
+    = V a
+
+    -- :-> Elimination
+    | App (Inf ty a) (Chk ty a)
+
+    -- :*: Elimination-1
+    | Fst (Inf ty a)
+
+    -- :*: Elimination-2
+    | Snd (Inf ty a)
+
+    -- annotated term
+    | Ann (Chk ty a) ty
+  deriving (Functor, Foldable, Traversable)
+
+(.:) :: Chk ty a -> ty -> Inf ty a
+(.:) = Ann
+infix 1 .:
+
+-- | Checkable terms
+data Chk ty a
+    -- Converted term
+    = Inf (Inf ty a)
+
+    -- :-> Introduction
+    | Lam (ScopeH () (Chk ty) (Inf ty) a)
+
+    -- :*: Introduction
+    | Pair (Chk ty a) (Chk ty a)
+
+    -- :+: Introduction-1
+    | Inl (Chk ty a)
+
+    -- :+: Introduction-2
+    | Inr (Chk ty a)
+
+    -- :+: Elimination
+    | Case (Inf ty a) (ScopeH () (Chk ty) (Inf ty) a) (ScopeH () (Chk ty) (Inf ty) a)
+
+  deriving (Functor, Foldable, Traversable)
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance IsString a => IsString (Inf ty a) where fromString = V . fromString
+instance IsString a => IsString (Chk ty a) where fromString = Inf . fromString
+
+instance Applicative (Inf ty) where
+    pure = V
+    (<*>) = ap
+
+instance Monad (Inf ty) where
+    return = V
+
+    V x      >>= k = k x
+    Ann x t  >>= k = Ann (x >>== k) t
+    App f x  >>= k = App (f >>= k) (x >>== k)
+    Fst x    >>= k = Fst (x >>= k)
+    Snd x    >>= k = Snd (x >>= k)
+
+instance ty ~ ty' => Module (Chk ty) (Inf ty') where
+    Inf x         >>== k = Inf (x >>= k)
+    Lam b         >>== k = Lam (b >>== k)
+    Pair x y      >>== k = Pair (x >>== k) (y >>== k)
+    Inl x         >>== k = Inl (x >>== k)
+    Inr y         >>== k = Inr (y >>== k)
+    Case e c1 c2  >>== k = Case (e >>= k) (c1 >>== k) (c2 >>== k)
+
+instance ty ~ ty' => LiftedModule (Chk ty) (Inf ty') where
+    mlift = Inf
+
+lam_ :: Eq a => a -> Chk ty a -> Chk ty a
+lam_ x b = Lam (abstract1H x b)
+
+case_ :: Eq a => Inf ty a -> a -> Chk ty a -> a -> Chk ty a -> Chk ty a
+case_ e x c1 y c2 = Case e (abstract1H x c1) (abstract1H y c2)
+
+-------------------------------------------------------------------------------
+-- Pretty
+-------------------------------------------------------------------------------
+
+instance Pretty Ty where
+    ppr = return . pprTy
+
+pprTy :: Ty -> Doc
+pprTy (Ty t)    = text (TS.unpack t)
+pprTy TUnit     = text "Unit"
+pprTy (a :*: b) = sexpr (text "prod") [pprTy a, pprTy b]
+pprTy (a :+: b) = sexpr (text "sum") [pprTy a, pprTy b]
+pprTy (a :-> b) = sexpr (text "->") $ map pprTy $ a : peelArr b
+
+instance (Pretty a, Pretty ty) => Pretty (Inf ty a) where ppr x = traverse ppr x >>= pprInf
+instance (Pretty a, Pretty ty) => Pretty (Chk ty a) where ppr x = traverse ppr x >>= pprChk
+
+pprInf :: Pretty ty => Inf ty Doc -> PrettyM Doc
+pprInf (V x) = pure x
+pprInf (App f x) = case peelApp f of
+    (f', xs) -> sexpr
+        <$> pprInf f'
+        <*> traverse pprChk (xs ++ [x])
+pprInf (Ann x t) = do
+    x' <- pprChk x
+    t' <- ppr t
+    return $ sexpr (text "the") [t', x']
+pprInf (Fst x)  = do
+    x' <- pprInf x
+    return $ sexpr (text "fst") [x']
+pprInf (Snd x)  = do
+    x' <- pprInf x
+    return $ sexpr (text "snd") [x']
+
+pprChk :: Pretty ty => Chk ty Doc -> PrettyM  Doc
+pprChk (Inf i) = pprInf i
+pprChk (Lam b) = do
+    n <- text <$> fresh "x"
+    b' <- pprChk (instantiate1H (V n) b)
+    return $ sexpr (text "fn") [ n, b' ]
+pprChk (Pair x y) = do
+    x' <- pprChk x    
+    y' <- pprChk y
+    return $ sexpr (text "pair") [x', y']
+pprChk (Inl x)  = do
+    x' <- pprChk x
+    return $ sexpr (text "inl") [x']
+pprChk (Inr x)  = do
+    x' <- pprChk x
+    return $ sexpr (text "inr") [x']
+pprChk (Case e c1 c2) = do
+    e' <- pprInf e
+    n1 <- text <$> fresh "x"
+    n2 <- text <$> fresh "y"
+    c1' <- pprChk (instantiate1H (V n1) c1)
+    c2' <- pprChk (instantiate1H (V n2) c2)
+    return $ sexpr (text "case+") [e', n1, c1', n2, c2']
+
+-- We output
+--   (0 1 2 3)
+-- instead of
+--   (((0 1) 2) 3)
+-- small, but nice improvement!
+peelApp :: Inf ty a -> (Inf ty a, [Chk ty a])
+peelApp (App a b)   = (++ [b]) <$> peelApp a
+peelApp e           = (e, [])
+
+peelArr :: Ty -> [Ty]
+peelArr (a :-> b) = a : peelArr b
+peelArr x         = [x]
+
+-------------------------------------------------------------------------------
+-- peelApp
+-------------------------------------------------------------------------------
+
+infixl 2 $$
+
+class SApp f g h | h -> f g where
+    ($$) :: f a -> g a -> h a
+
+instance SApp (Inf ty) (Chk ty) (Inf ty) where ($$) = App
+instance SApp (Inf ty) (Chk ty) (Chk ty) where f $$ x = Inf (f $$ x)
+
+-------------------------------------------------------------------------------
+-- Normal form
+-------------------------------------------------------------------------------
+
+nfApp :: Chk ty a -> Chk ty a -> Maybe (Chk ty a)
+nfApp (Inf f) x = Just $ Inf (App f x)
+nfApp (Lam b) x        = chkBind (fromScopeH b) (unvar (const x) (Inf . V))
+nfApp Pair {} _        = Nothing
+nfApp Inl {}  _        = Nothing
+nfApp Inr {}  _        = Nothing
+nfApp (Case e c1 c2) x = do
+    let x' = fmap F x
+    c1' <- nfApp (fromScopeH c1) x'
+    c2' <- nfApp (fromScopeH c2) x'
+    Just $ Case e (toScopeH c1') (toScopeH c2')
+
+nfFst :: Chk ty b -> Maybe (Chk ty b)
+nfFst (Inf x)        = Just $ Inf (Fst x)
+nfFst (Pair x _)     = Just x
+nfFst Lam {}         = Nothing
+nfFst Inl {}         = Nothing
+nfFst Inr {}         = Nothing
+nfFst (Case e c1 c2) = do
+    c1' <- nfFst (fromScopeH c1)
+    c2' <- nfFst (fromScopeH c2)
+    Just $ Case e (toScopeH c1') (toScopeH c2')
+
+nfSnd :: Chk ty b -> Maybe (Chk ty b)
+nfSnd (Inf x)        = Just $ Inf (Snd x)
+nfSnd (Pair x _)     = Just x
+nfSnd Lam {}         = Nothing
+nfSnd Inl {}         = Nothing
+nfSnd Inr {}         = Nothing
+nfSnd (Case e c1 c2) = do
+    c1' <- nfSnd (fromScopeH c1)
+    c2' <- nfSnd (fromScopeH c2)
+    Just $ Case e (toScopeH c1') (toScopeH c2')
+
+nfCase :: Chk ty a -> Chk ty (Var () a) -> Chk ty (Var () a) -> Maybe (Chk ty a)
+nfCase (Inf e)        c1 c2 = Just $ Case e (toScopeH c1) (toScopeH c2)
+nfCase (Inl x)        c1 _  = chkBind c1 (unvar (const x) (Inf . V))
+nfCase (Inr y)        _  c2 = chkBind c2 (unvar (const y) (Inf . V))
+nfCase Lam {}         _  _  = Nothing
+nfCase Pair {}        _  _  = Nothing
+nfCase (Case e d1 d2) c1 c2 = do
+    let mkCase c = nfCase c (fmap F $ fromScopeH d1) (fmap F $ fromScopeH d2)
+    c1' <- mkCase c1
+    c2' <- mkCase c2
+    Just $ Case e (toScopeH c1') (toScopeH c2') 
+
+infBind :: Inf ty a -> (a -> Chk ty b) -> Maybe (Chk ty b)
+infBind (Ann x _) k = chkBind x k
+infBind (V x)     k = Just $ k x
+infBind (App f x) k = do 
+    f' <- infBind f k
+    x' <- chkBind x k
+    nfApp f' x'
+infBind (Fst x)   k = do
+    x' <- infBind x k
+    nfFst x'
+infBind (Snd x)   k = do
+    x' <- infBind x k
+    nfSnd x'
+
+chkBind :: Chk ty a -> (a -> Chk ty b) -> Maybe (Chk ty b)
+chkBind (Inf a) k = infBind a k
+chkBind (Lam b) k = do
+    b' <- chkBind (fromScopeH b) (unvar (Inf . V . B) (fmap F . k))
+    return $ Lam $ toScopeH b'
+chkBind (Pair x y) k = do
+    x' <- chkBind x k
+    y' <- chkBind y k
+    return $ Pair x' y'
+chkBind (Inl x) k = do
+    x' <- chkBind x k
+    return $ Inl x'
+chkBind (Inr y) k = do
+    y' <- chkBind y k
+    return $ Inl y'
+chkBind (Case e c1 c2) k = do
+    e' <- infBind e k
+    c1' <- chkBind (fromScopeH c1) (unvar (Inf . V . B) (fmap F . k))
+    c2' <- chkBind (fromScopeH c2) (unvar (Inf . V . B) (fmap F . k))
+    nfCase e' c1' c2'
+
+-------------------------------------------------------------------------------
+-- Type-checking
+-------------------------------------------------------------------------------
+
+infer :: (a -> Ty) -> Inf Ty a -> Maybe (Chk Void a, Ty)
+infer f = infer' . fmap (\x -> (x, f x))
+
+-- No error reporting :)
+infer' :: Inf Ty (a, Ty) -> Maybe (Chk Void a, Ty)
+infer' (V (a, at)) = Just (Inf (V a), at)
+infer' (Ann x t) = do
+    x' <- check' x t
+    Just (x', t)
+infer' (App f x) = do
+    (f', ft) <- infer' f
+    case ft of
+        a :-> b -> do
+            x' <- check' x a
+            t <- nfApp f' x'
+            return (t, b)
+        _       -> Nothing
+infer' (Fst x) = do
+    (x', xt) <- infer' x
+    case xt of
+        (a :*: _) -> do
+            t <- nfFst x'
+            return (t, a)
+        _ -> Nothing
+infer' (Snd x) = do
+    (x', xt) <- infer' x
+    case xt of
+        (_ :*: b) -> do
+            t <- nfSnd x'
+            return (t, b)
+        _ -> Nothing
+
+check' :: Chk Ty (a, Ty) -> Ty -> Maybe (Chk Void a)
+check' (Lam x) t = case t of
+    a :-> b -> do
+        let xx = fmap (unvar (\n -> (B n, a)) (first F)) $ fromScopeH x
+        xx' <- check' xx b
+        return $ Lam (toScopeH xx')
+    _ -> Nothing
+check' (Inf x) t = do
+    (x', xt) <- infer' x
+    if t == xt
+    then Just x'
+    else Nothing
+check' (Pair x y) t = case t of
+    a :*: b -> do
+        x' <- check' x a
+        y' <- check' y b
+        return (Pair x' y')
+    _ -> Nothing
+check' (Inl x) t = case t of
+    a :+: _ -> do
+        x' <- check' x a
+        return (Inl x')
+    _ -> Nothing
+check' (Inr y) t = case t of
+    _ :+: b -> do
+        y' <- check' y b
+        return (Inl y')
+    _ -> Nothing
+check' (Case e c1 c2) t = do
+    (e', et) <- infer' e
+    case et of
+        a :+: b -> do
+            let cc1 = fmap (unvar (\n -> (B n, a)) (first F)) $ fromScopeH c1
+            let cc2 = fmap (unvar (\n -> (B n, b)) (first F)) $ fromScopeH c2
+            cc1' <- check' cc1 t
+            cc2' <- check' cc2 t
+            nfCase e' cc1' cc2'
+        _ -> Nothing
+
+-------------------------------------------------------------------------------
+-- Examples
+-------------------------------------------------------------------------------
+
+demo :: String -> Inf Ty ShortText -> [String]
+demo name e = case infer ctx e of
+    Nothing ->
+        [ name ++ " = " ++ pretty e
+        , "DOESN'T TYPECHECK"
+        ]
+    Just (nf, t) ->
+        [ name ++ " : " ++ pretty t
+        , name ++ " = " ++ pretty e
+        , name ++ " = " ++ pretty nf
+        ]
+  where
+    ctx "f"   = "A" :-> "B"
+    ctx "a"   = "A"
+    ctx "b"   = "B"
+    ctx "c" = "C"
+    ctx "a2c" = "A" :-> "C"
+    ctx "b2c" = "B" :-> "C"
+    ctx "aorb" = "A" :+: "B"
+    ctx "ac2d" = "A" :-> "C" :-> "D"
+    ctx "bc2d" = "B" :-> "C" :-> "D"
+    ctx "aa2b" = "A" :-> "A" :-> "B"
+    ctx _     = TUnit
+
+tests :: TestTree
+tests = testGroup "Bi-directional STLC 2"
+    [ demo' "arr-beta"  $ (lam_ "x" ("f" $$ "x") .: "A" :-> "B") $$ "a"
+    , demo' "pair-beta" $ Fst (Pair "a" "b" .: "A" :*: "B")
+    , demo' "sum-beta"  $ case_ (Inl "a" .: "A" :+: "B") "x" ("a2c" $$ "x") "y" ("b2c" $$ "y") .: "C"
+    , demo' "app-delta" $ (case_ "aorb" "x" ("ac2d" $$"x") "y" ("bc2d" $$ "y") .: "C" :-> "D") $$ "c"
+    , demo' "redundant-case" $
+        (case_ "aorb" "x" (case_ "aorb" "u" ("aa2b" $$ "x" $$ "u") "v" "v") "y" "y".: "B")
+    ]
+  where
+    demo' name e = goldenVsString name ("examples" </> name' -<.> "txt")
+        $ return $ UTF8.fromString $ unlines
+        $ demo name e
+      where
+        name' = "stlc-2-" ++ name
+
diff --git a/examples/BiSTLC3.hs b/examples/BiSTLC3.hs
new file mode 100644
--- /dev/null
+++ b/examples/BiSTLC3.hs
@@ -0,0 +1,398 @@
+{-# LANGUAGE DeriveFoldable         #-}
+{-# LANGUAGE DeriveFunctor          #-}
+{-# LANGUAGE DeriveTraversable      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE OverloadedStrings      #-}
+module BiSTLC3 (tests) where
+
+import Bound.ScopeH
+import Bound.Var            (Var (..), unvar)
+import Control.Monad        (ap)
+import Control.Monad.Module
+import Data.Bifunctor       (first)
+import Data.String          (IsString (..))
+import System.FilePath      ((-<.>), (</>))
+import Test.Tasty           (TestTree, testGroup)
+import Test.Tasty.Golden    (goldenVsString)
+
+import qualified Data.ByteString.Lazy.UTF8 as UTF8
+import qualified Data.Text.Short           as TS
+
+import Pretty
+
+-------------------------------------------------------------------------------
+-- Types
+-------------------------------------------------------------------------------
+
+-- | Types.
+data Ty
+    = Ty ShortText
+    | TUnit
+    | Ty :*: Ty
+    | Ty :-> Ty
+  deriving Eq
+
+infixr 2 :->
+infix 4 :*:
+
+instance IsString Ty where
+    fromString = Ty . fromString
+
+-------------------------------------------------------------------------------
+-- Elimession
+-------------------------------------------------------------------------------
+
+-- | Elimerable terms
+data Elim a
+    -- Variable
+    = Var a
+
+    -- :-> Elimination
+    | App (Elim a) (Term a)
+
+    -- :*: Elimination-1
+    | Fst (Elim a)
+
+    -- :*: Elimination-2
+    | Snd (Elim a)
+
+    -- annotated term
+    | Ann (Term a) Ty
+  deriving (Functor, Foldable, Traversable)
+
+(.:) :: Term a -> Ty -> Elim a
+(.:) = Ann
+infix 1 .:
+
+-- | Checkable terms
+data Term a
+    -- Converted term
+    = Emb (Elim a)
+
+    -- :-> Introduction
+    | Lam (ScopeH () Term Elim a)
+
+    -- :*: Introduction
+    | Mul (Term a) (Term a)
+
+  deriving (Functor, Foldable, Traversable)
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance IsString a => IsString (Elim a) where fromString = Var . fromString
+instance IsString a => IsString (Term a) where fromString = Emb . fromString
+
+instance Applicative Elim where
+    pure = Var
+    (<*>) = ap
+
+instance Monad Elim where
+    return = Var
+
+    Var x      >>= k = k x
+    Ann x t  >>= k = Ann (x >>== k) t
+    App f x  >>= k = App (f >>= k) (x >>== k)
+    Fst x    >>= k = Fst (x >>= k)
+    Snd x    >>= k = Snd (x >>= k)
+
+instance Module Term Elim where
+    Emb x    >>== k = Emb (x >>= k)
+    Lam b    >>== k = Lam (b >>== k)
+    Mul x y  >>== k = Mul (x >>== k) (y >>== k)
+
+instance LiftedModule Term Elim where
+    mlift = Emb
+
+lam_ :: Eq a => a -> Term a -> Term a
+lam_ x b = Lam (abstract1H x b)
+
+-------------------------------------------------------------------------------
+-- Pretty
+-------------------------------------------------------------------------------
+
+instance Pretty Ty where
+    ppr = return . pprTy
+
+pprTy :: Ty -> Doc
+pprTy (Ty t)    = text (TS.unpack t)
+pprTy TUnit     = text "Unit"
+pprTy (a :*: b) = sexpr (text "prod") [pprTy a, pprTy b]
+pprTy (a :-> b) = sexpr (text "->") $ map pprTy $ a : peelArr b
+
+instance Pretty a => Pretty (Elim a) where ppr x = traverse ppr x >>= pprElim
+instance Pretty a => Pretty (Term a) where ppr x = traverse ppr x >>= pprTerm
+
+pprElim :: Elim Doc -> PrettyM Doc
+pprElim (Var x) = pure x
+pprElim (App f x) = case peelApp f of
+    (f', xs) -> sexpr
+        <$> pprElim f'
+        <*> traverse pprTerm (xs ++ [x])
+pprElim (Ann x t) = do
+    x' <- pprTerm x
+    t' <- ppr t
+    return $ sexpr (text "the") [t', x']
+pprElim (Fst x)  = do
+    x' <- pprElim x
+    return $ sexpr (text "fst") [x']
+pprElim (Snd x)  = do
+    x' <- pprElim x
+    return $ sexpr (text "snd") [x']
+
+pprTerm :: Term Doc -> PrettyM  Doc
+pprTerm (Emb e) = pprElim e
+pprTerm (Lam b) = do
+    n <- text <$> fresh "x"
+    b' <- pprTerm (instantiate1H (Var n) b)
+    return $ sexpr (text "fn") [ n, b' ]
+pprTerm (Mul x y) = do
+    x' <- pprTerm x    
+    y' <- pprTerm y
+    return $ sexpr (text "pair") [x', y']
+
+-- We output
+--   (0 1 2 3)
+-- instead of
+--   (((0 1) 2) 3)
+-- small, but nice improvement!
+peelApp :: Elim a -> (Elim a, [Term a])
+peelApp (App a b)   = (++ [b]) <$> peelApp a
+peelApp e           = (e, [])
+
+peelArr :: Ty -> [Ty]
+peelArr (a :-> b) = a : peelArr b
+peelArr x         = [x]
+
+-------------------------------------------------------------------------------
+-- peelApp
+-------------------------------------------------------------------------------
+
+infixl 2 $$
+
+class SApp f g h | h -> f g where
+    ($$) :: f a -> g a -> h a
+
+instance SApp Elim Term Elim where ($$) = App
+instance SApp Elim Term Term where f $$ x = Emb (f $$ x)
+
+-------------------------------------------------------------------------------
+-- Normal form
+-------------------------------------------------------------------------------
+
+data NFElim a
+    = NFElimNeu (UNeut a)
+    | NFElimAnn (NFTerm a) Ty
+  deriving (Functor, Foldable, Traversable)
+
+data NFTerm a
+    = NFEmb (UNeut a)
+    | NFLam (ScopeH () NFTerm NFElim a)
+    | NFMul (NFTerm a) (NFTerm a)
+  deriving (Functor, Foldable, Traversable)
+
+-- | Upsilon neutral eliminations
+data UNeut a
+    = NFVar a
+    | NFApp (BNeut a) (NFTerm a)
+    | NFFst (BNeut a)
+    | NFSnd (BNeut a)
+    | NFEvalPanic
+  deriving (Functor, Foldable, Traversable)
+
+-- | Beta neutral eliminations
+data BNeut a
+    = BNeutNeu (UNeut a)
+    | BNeutAnnEmb (UNeut a) Ty
+  deriving (Functor, Foldable, Traversable)
+
+nfVar :: a -> NFElim a
+nfVar = NFElimNeu . NFVar
+
+nfApp :: NFElim a -> NFTerm a -> NFElim a
+nfApp (NFElimNeu f)                   s =
+    NFElimNeu (NFApp (BNeutNeu f) s)
+nfApp (NFElimAnn (NFLam t) (a :-> b)) s =
+    NFElimAnn (instantiate1H (NFElimAnn s a) t) b
+nfApp (NFElimAnn (NFEmb u) ty) s =
+    NFElimNeu (NFApp (BNeutAnnEmb u ty) s)
+nfApp _ _ = NFElimNeu NFEvalPanic
+
+nfFst :: NFElim a -> NFElim a
+nfFst (NFElimNeu e) =
+    NFElimNeu (NFFst (BNeutNeu e))
+nfFst (NFElimAnn (NFMul t _) (a :*: _)) =
+    NFElimAnn t a
+nfFst (NFElimAnn (NFEmb u) ty) =
+    NFElimNeu (NFFst (BNeutAnnEmb u ty))
+nfFst _ = NFElimNeu NFEvalPanic
+
+nfSnd :: NFElim a -> NFElim a
+nfSnd (NFElimNeu e) =
+    NFElimNeu (NFSnd (BNeutNeu e))
+nfSnd (NFElimAnn (NFMul _ s) (_ :*: b)) =
+    NFElimAnn s b
+nfSnd (NFElimAnn (NFEmb u) ty) =
+    NFElimNeu (NFSnd (BNeutAnnEmb u ty))
+nfSnd _ = NFElimNeu NFEvalPanic
+
+nfAnn :: NFTerm a -> Ty -> NFElim a
+nfAnn = NFElimAnn
+
+nfEmb :: NFElim a -> NFTerm a
+nfEmb (NFElimNeu u) = NFEmb u
+nfEmb (NFElimAnn t _) = t -- upsilon-reduction
+
+instance Applicative NFElim where
+    pure = nfVar
+    (<*>) = ap
+
+instance Monad NFElim where
+    return = nfVar
+
+    NFElimNeu e   >>= k = substU e k
+    NFElimAnn t a >>= k = NFElimAnn (t >>== k) a
+
+substU :: UNeut a -> (a -> NFElim b) -> NFElim b
+substU (NFVar x)   k = k x
+substU (NFApp f s) k = nfApp (substB f k) (s >>== k)
+substU (NFFst e)   k = nfFst (substB e k)
+substU (NFSnd e)   k = nfSnd (substB e k)
+substU NFEvalPanic _ = NFElimNeu NFEvalPanic
+
+substB :: BNeut a -> (a -> NFElim b) -> NFElim b
+substB (BNeutNeu e)       k = substU e k
+substB (BNeutAnnEmb e ty) k = nfAnn (nfEmb (substU e k)) ty
+
+instance Module NFTerm NFElim where
+    NFEmb u   >>== k = nfEmb (substU u k)
+    NFLam b   >>== k = NFLam (b >>== k)
+    NFMul t s >>== k = NFMul (t >>== k) (s >>== k)
+
+-------------------------------------------------------------------------------
+-- From normal forms to terms
+-------------------------------------------------------------------------------
+
+class ToTerm t where toTerm :: t a -> Term a
+class ToElim t where toElim :: t a -> Elim a
+
+instance ToTerm Term where toTerm = id
+instance ToElim Elim where toElim = id
+
+instance ToElim NFElim where
+    toElim (NFElimNeu e)   = toElim e
+    toElim (NFElimAnn t a) = Ann (toTerm t) a
+
+instance ToElim BNeut where
+    toElim (BNeutNeu e)       = toElim e
+    toElim (BNeutAnnEmb e ty) = Ann (Emb (toElim e)) ty
+
+instance ToElim UNeut where
+    toElim (NFVar a)   = Var a
+    toElim (NFApp f s) = App (toElim f) (toTerm s)
+    toElim (NFFst e)   = Fst (toElim e)
+    toElim (NFSnd e)   = Snd (toElim e)
+    toElim NFEvalPanic = error "eval panic"
+
+instance ToTerm NFTerm where
+    toTerm (NFEmb e)   = Emb (toElim e)
+    toTerm (NFLam t)   = Lam (toScopeH (toTerm (fromScopeH t)))
+    toTerm (NFMul t s) = Mul (toTerm t) (toTerm s)
+
+
+-------------------------------------------------------------------------------
+-- Type-checking
+-------------------------------------------------------------------------------
+
+-- infer and check return evaluated values as well.
+
+infer :: (a -> Ty) -> Elim a -> Maybe (NFElim a, Ty)
+infer f = infer' . fmap (\x -> (x, f x))
+
+-- No error reporting :)
+infer' :: Elim (a, Ty) -> Maybe (NFElim a, Ty)
+infer' (Var (a, at)) = Just (nfVar a, at)
+infer' (Ann x t) = do
+    x' <- check' x t
+    Just (nfAnn x' t, t)
+infer' (App f x) = do
+    (f', ft) <- infer' f
+    case ft of
+        a :-> b -> do
+            x' <- check' x a
+            return (nfApp f' x', b)
+        _       -> Nothing
+infer' (Fst x) = do
+    (x', xt) <- infer' x
+    case xt of
+        (a :*: _) -> do
+            return (nfFst x', a)
+        _ -> Nothing
+infer' (Snd x) = do
+    (x', xt) <- infer' x
+    case xt of
+        (_ :*: b) -> do
+            return (nfSnd x', b)
+        _ -> Nothing
+
+check' :: Term (a, Ty) -> Ty -> Maybe (NFTerm a)
+check' (Lam x) t = case t of
+    a :-> b -> do
+        let xx = fmap (unvar (\n -> (B n, a)) (first F)) $ fromScopeH x
+        xx' <- check' xx b
+        return $ NFLam (toScopeH xx')
+    _ -> Nothing
+check' (Emb x) t = do
+    (x', xt) <- infer' x
+    if t == xt
+    then Just (nfEmb x')
+    else Nothing
+check' (Mul x y) t = case t of
+    a :*: b -> do
+        x' <- check' x a
+        y' <- check' y b
+        return (NFMul x' y')
+    _ -> Nothing
+
+-------------------------------------------------------------------------------
+-- Examples
+-------------------------------------------------------------------------------
+
+demo :: String -> Elim ShortText -> [String]
+demo name e = case infer ctx e of
+    Nothing ->
+        [ name ++ " = " ++ pretty e
+        , "DOESN'T TYPECHECK"
+        ]
+    Just (nf, t) ->
+        [ name ++ " : " ++ pretty t
+        , name ++ " = " ++ pretty e
+        , name ++ " = " ++ pretty (toElim nf)
+        ]
+  where
+    ctx "f"   = "A" :-> "B"
+    ctx "a"   = "A"
+    ctx "b"   = "B"
+    ctx "c" = "C"
+    ctx "a2c" = "A" :-> "C"
+    ctx "b2c" = "B" :-> "C"
+    ctx "ac2d" = "A" :-> "C" :-> "D"
+    ctx "bc2d" = "B" :-> "C" :-> "D"
+    ctx "aa2b" = "A" :-> "A" :-> "B"
+    ctx _     = TUnit
+
+tests :: TestTree
+tests = testGroup "Bi-directional STLC 3"
+    [ demo' "arr-beta"  $ (lam_ "x" ("f" $$ "x") .: "A" :-> "B") $$ "a"
+    , demo' "pair-beta" $ Fst (Mul "a" "b" .: "A" :*: "B")
+    ]
+  where
+    demo' name e = goldenVsString name ("examples" </> name' -<.> "txt")
+        $ return $ UTF8.fromString $ unlines
+        $ demo name e
+      where
+        name' = "stlc-3-" ++ name
+
diff --git a/examples/Examples.hs b/examples/Examples.hs
--- a/examples/Examples.hs
+++ b/examples/Examples.hs
@@ -1,6 +1,8 @@
 module Main (main) where
 
 import qualified BiSTLC
+import qualified BiSTLC2
+import qualified BiSTLC3
 import qualified SystemF
 
 import Test.Tasty           (testGroup, defaultMain)
@@ -8,5 +10,7 @@
 main :: IO ()
 main = defaultMain $ testGroup "Examples"
     [ BiSTLC.tests
+    , BiSTLC2.tests
+    , BiSTLC3.tests
     , SystemF.tests
     ]
diff --git a/examples/Pretty.hs b/examples/Pretty.hs
--- a/examples/Pretty.hs
+++ b/examples/Pretty.hs
@@ -11,8 +11,9 @@
     ) where
 
 import Control.Monad.Trans.State.Strict
+import Data.Char                        (isDigit)
 import Data.Text.Short                  (ShortText)
-import Data.Char (isDigit)
+import Data.Void                        (Void, absurd)
 
 import qualified Data.Text.Short  as TS
 import qualified Text.PrettyPrint as PP
@@ -61,3 +62,6 @@
     ppr t = do
         markUsed t
         return $ PP.text $ TS.unpack t
+
+instance Pretty Void where
+    ppr = absurd
diff --git a/examples/stlc-2-app-delta.txt b/examples/stlc-2-app-delta.txt
new file mode 100644
--- /dev/null
+++ b/examples/stlc-2-app-delta.txt
@@ -0,0 +1,3 @@
+app-delta : D
+app-delta = ((the (-> C D) (case+ aorb x (ac2d x) y (bc2d y))) c)
+app-delta = (case+ aorb x (ac2d x c) y (bc2d y c))
diff --git a/examples/stlc-2-arr-beta.txt b/examples/stlc-2-arr-beta.txt
new file mode 100644
--- /dev/null
+++ b/examples/stlc-2-arr-beta.txt
@@ -0,0 +1,3 @@
+arr-beta : B
+arr-beta = ((the (-> A B) (fn x (f x))) a)
+arr-beta = (f a)
diff --git a/examples/stlc-2-pair-beta.txt b/examples/stlc-2-pair-beta.txt
new file mode 100644
--- /dev/null
+++ b/examples/stlc-2-pair-beta.txt
@@ -0,0 +1,3 @@
+pair-beta : A
+pair-beta = (fst (the (prod A B) (pair a b)))
+pair-beta = a
diff --git a/examples/stlc-2-redundant-case.txt b/examples/stlc-2-redundant-case.txt
new file mode 100644
--- /dev/null
+++ b/examples/stlc-2-redundant-case.txt
@@ -0,0 +1,3 @@
+redundant-case : B
+redundant-case = (the B (case+ aorb x (case+ aorb x0 (aa2b x x0) y0 y0) y y))
+redundant-case = (case+ aorb x (case+ aorb x0 (aa2b x x0) y0 y0) y y)
diff --git a/examples/stlc-2-sum-beta.txt b/examples/stlc-2-sum-beta.txt
new file mode 100644
--- /dev/null
+++ b/examples/stlc-2-sum-beta.txt
@@ -0,0 +1,3 @@
+sum-beta : C
+sum-beta = (the C (case+ (the (sum A B) (inl a)) x (a2c x) y (b2c y)))
+sum-beta = (a2c a)
diff --git a/examples/stlc-3-arr-beta.txt b/examples/stlc-3-arr-beta.txt
new file mode 100644
--- /dev/null
+++ b/examples/stlc-3-arr-beta.txt
@@ -0,0 +1,3 @@
+arr-beta : B
+arr-beta = ((the (-> A B) (fn x (f x))) a)
+arr-beta = (the B (f a))
diff --git a/examples/stlc-3-pair-beta.txt b/examples/stlc-3-pair-beta.txt
new file mode 100644
--- /dev/null
+++ b/examples/stlc-3-pair-beta.txt
@@ -0,0 +1,3 @@
+pair-beta : A
+pair-beta = (fst (the (prod A B) (pair a b)))
+pair-beta = (the A a)
diff --git a/src/Bound/ScopeH.hs b/src/Bound/ScopeH.hs
--- a/src/Bound/ScopeH.hs
+++ b/src/Bound/ScopeH.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE UndecidableInstances  #-}
 -- | 'ScopeH' scope, which allows substitute 'f' into 'g' to get new 'g'.
 --
@@ -17,7 +18,7 @@
 -- we diffentiate between @Poly@ and @Mono@-morphic types.
 --
 -- @
--- specialise :: Poly a -> Mono a -> Poly a 
+-- specialise :: Poly a -> Mono a -> Poly a
 -- specialise (Forall p) m = 'instantiate1H' m p
 -- specialise _          _ = error "ill-kinded"
 -- @
@@ -25,7 +26,7 @@
 -- Another applications are /bidirectional/ type-systems or representing
 -- normal forms with /normal/ and  /neutral/ terms,
 -- aka /introduction/ and /elimination/ terms.
---  
+--
 -- Look into @examples/@ directory for /System F/ and /Bidirectional STLC/
 -- implemented with a help of 'ScopeH'.
 --
@@ -37,6 +38,8 @@
     abstractHName, abstract1HName,
     -- * Instantiation
     instantiateH, instantiate1H, instantiateHEither,
+    -- * Lifting
+    liftScopeH,
     -- * Traditional de Bruijn
     fromScopeH,
     toScopeH,
@@ -60,7 +63,7 @@
 import Bound                (Scope (..), Var (..))
 import Bound.Name           (Name (..))
 import Control.DeepSeq      (NFData (..))
-import Control.Monad.Module (Module (..))
+import Control.Monad.Module (Module (..), LiftedModule (..))
 import Data.Bifoldable      (bifoldMap, bitraverse_)
 import Data.Bifunctor       (bimap)
 import Data.Bitraversable   (Bitraversable (..))
@@ -82,6 +85,9 @@
 instance (Functor f, Monad m) => Module (ScopeH b f m) m where
     ScopeH s >>== k = ScopeH $ fmap (fmap (>>= k)) s
 
+instance LiftedModule f m => LiftedModule (ScopeH b f m) m where
+    mlift = liftScopeH
+
 -------------------------------------------------------------------------------
 -- Instances
 -------------------------------------------------------------------------------
@@ -199,9 +205,20 @@
 -- | Enter a 'ScopeH', and instantiate all bound and free variables in one go.
 instantiateHEither :: Module f m => (Either b a -> m c) -> ScopeH b f m a -> f c
 instantiateHEither f (ScopeH e) = e >>== \v -> case v of
-    B b -> f (Left b)
+    B b  -> f (Left b)
     F ea -> ea >>= f . Right
 {-# INLINE instantiateHEither #-}
+
+-------------------------------------------------------------------------------
+-- Lifting
+-------------------------------------------------------------------------------
+
+-- |
+--
+-- @since 0.0.2
+liftScopeH:: forall f m a b. LiftedModule f m => m a -> ScopeH b f m a
+liftScopeH m = ScopeH (mlift (return (F m) :: m (Var b (m a))))
+{-# INLINE liftScopeH #-}
 
 -------------------------------------------------------------------------------
 -- Traditional de Bruijn
diff --git a/src/Bound/ScopeT.hs b/src/Bound/ScopeT.hs
--- a/src/Bound/ScopeT.hs
+++ b/src/Bound/ScopeT.hs
@@ -20,6 +20,8 @@
     abstractTName, abstract1TName,
     -- * Instantiation
     instantiateT, instantiate1T, instantiateTEither,
+    -- * Lifting
+    liftScopeT,
     -- * Traditional de Bruijn
     fromScopeT,
     toScopeT,
@@ -41,7 +43,7 @@
 import Bound                (Bound (..), Scope (..), Var (..))
 import Bound.Name           (Name (..))
 import Control.DeepSeq      (NFData (..))
-import Control.Monad.Module (Module (..))
+import Control.Monad.Module (Module (..), LiftedModule (..))
 import Data.Bifoldable      (bifoldMap, bitraverse_)
 import Data.Bifunctor       (bimap)
 import Data.Bitraversable   (Bitraversable (..))
@@ -88,6 +90,14 @@
 instance (Monad f, Functor (t f)) => Module (ScopeT b t f) f where
     (>>==) = (>>>>=)
 
+instance (Monad f, Monad (t f)) => LiftedModule (ScopeT b t f) f where
+    mlift = liftScopeT
+
+-- we can define this, as we need Monad (t m).
+-- QuantifiedConstraint for transformers would solve that.
+-- instance MonadTrans (ScopeT b t) where
+--     lift = mlift
+
 instance (Hashable b, Bound t, Monad f, Hashable1 f, Hashable1 (t f)) => Hashable1 (ScopeT b t f) where
     liftHashWithSalt h s m = liftHashWithSalt (liftHashWithSalt h) s (fromScopeT m)
     {-# INLINE liftHashWithSalt #-}
@@ -197,6 +207,17 @@
     B b -> f (Left b)
     F ea -> ea >>= f . Right
 {-# INLINE instantiateTEither #-}
+
+-------------------------------------------------------------------------------
+-- Lifting
+-------------------------------------------------------------------------------
+
+-- |
+--
+-- @since 0.0.2
+liftScopeT:: forall t f a b. (Monad (t f)) => f a -> ScopeT b t f a
+liftScopeT = ScopeT . return . F
+{-# INLINE liftScopeT #-}
 
 -------------------------------------------------------------------------------
 -- Traditional de Bruijn
diff --git a/src/Control/Monad/Module.hs b/src/Control/Monad/Module.hs
--- a/src/Control/Monad/Module.hs
+++ b/src/Control/Monad/Module.hs
@@ -54,3 +54,13 @@
 
 instance Monad m => Module (Scope b m) m where
     (>>==) = (>>>=)
+
+-- | An extension of 'Module' allowing to lift @m a@ info @f a@.
+-- As we have @'Monad' m@, this allows to have a pseudo-return for @f@:
+-- @point . return :: a -> f a@
+--
+-- /Note:/ for @f = t m@ for some @'MonadTrans' t@ @'mlift' = 'lift'@.
+--
+-- @since 0.0.2
+class Module f m => LiftedModule f m where
+    mlift :: m a -> f a