diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -8,6 +8,11 @@
 
 a tiny statically typed functional programming language.
 
+## Installation
+
+* brew install z3
+* cabal install ntha
+
 ## Features
 
 * Global type inference with optional type annotations.
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -37,7 +37,7 @@
   EProgram instructions -> do
     let imports = filter isImport instructions
     let continueAst = EProgram $ filter (not . isImport) instructions
-    importEnv <- foldM (\env (EImport path) -> loadFile env path) env imports
+    importEnv <- foldM (\ev (EImport path) -> loadFile ev path) env imports
     return (importEnv, continueAst)
   _ -> return (env, expr)
 
diff --git a/examples/misc.ntha b/examples/misc.ntha
new file mode 100644
--- /dev/null
+++ b/examples/misc.ntha
@@ -0,0 +1,195 @@
+;; recursive function
+
+(ƒ penultimate [xs]
+  (match xs
+    ([] ⇒ 0)
+    ([_] ⇒ 0)
+    ([a _] ⇒ a)
+    (_ :: t ⇒ (penultimate t))))
+
+(fib : Z → Z)
+(ƒ fib [x]
+  (match x
+    (0 ⇒ 0)
+    (1 ⇒ 1)
+    (_ ⇒ (+ (fib (- x 1)) (fib (- x 2))))))
+
+(asserteq (fib 5) 5)
+(print (int2str (fib 5)))
+
+(ƒ fibc [x]
+  (cond
+    ((= x 0) ⇒ 0)
+    ((= x 1) ⇒ 1)
+    (else ⇒ (+ (fibc (- x 1)) (fibc (- x 2))))))
+
+(asserteq (fibc 5) 5)
+(print (int2str (fibc 5)))
+
+(ƒ fact [n]
+  (if (≤ n 1)
+    1
+    (* n (fact (- n 1)))))
+
+(let f5 (fact 5))
+
+(asserteq f5 120)
+(print (int2str f5))
+
+(ƒ fact-wrap [n]
+  (let [fact (λ n → (if (≤ n 1)
+                         1
+                         (* n (fact (- n 1)))))]
+    (fact n)))
+
+(let f5 (fact-wrap 5))
+(print (int2str f5))
+
+(ƒ factc [n]
+  (cond
+    ((≤ n 1) → 1)
+    (else → (* n (factc (- n 1))))))
+
+(let fc5 (factc 5))
+
+(asserteq fc5 120)
+(print (int2str fc5))
+
+;; record data type
+
+(let profile {:name "ntha" :age 3})
+
+(asserteq (:name profile) "ntha")
+(print (:name profile))
+
+;; destructuring
+
+(let (a . b) (4 . "d"))
+
+(let d ((4 . true) . ("test" . 'c' . a)))
+
+(let ((_ . bool) . (_ . _ . _)) d)
+
+(asserteq bool true)
+(print (bool2str bool))
+
+;; algebraic data type and pattern matching
+
+(data Tree a Empty-Tree (Leaf a) (Node (Tree a) a (Tree a)))
+
+(let t (Node (Leaf 5) 4 (Leaf 3)))
+
+(depth : (Tree α) → Z)
+(ƒ depth
+  [t]
+  (match t
+    (Empty-Tree => 0)
+    ((Leaf _) => 1)
+    ((Node l _ r)  => (inc (max (depth l) (depth r))))))
+
+(asserteq (depth t) 2)
+
+(print (int2str (depth t)))
+
+(asserteq (depth (Leaf 3)) 1)
+
+(print (int2str (depth (Leaf 3))))
+
+(asserteq (depth Empty-Tree) 0)
+
+(print (int2str (depth Empty-Tree)))
+
+;; lambda and high-order function
+
+(let l [1 2])
+
+(ƒ double [x] (* 2 x))
+
+(let ll1 (map double l))
+
+(asserteq ll1 [2 4])
+
+(let ll2 (map (λ x => (* 2 x)) l))
+
+(asserteq ll2 [2 4])
+
+(let l2 [[1 2 3] [4 5 6]])
+
+(asserteq (map len l2) [3 3])
+
+;; curried function
+
+(ƒ add [x y] (+ x y))
+
+(let inc (add 1))
+
+(let three (inc 2))
+
+(asserteq three 3)
+
+(print (int2str three))
+
+;; lexical scope
+
+(let a 3)
+
+(let f (λ x → (* a x)))
+
+(let a 5)
+
+(asserteq (f 5) 15)
+
+(print (int2str (f 5)))
+
+;; monad
+
+(let m (do Maybe
+         (a <- (Just 3))
+         (b <- (Just (+ a 3)))
+         (return (* b 3))))
+
+(asserteq m (Just 18))
+
+(begin
+  (let name "ntha")
+  (print name)
+  (print "language"))
+
+;; negative number
+
+(asserteq (+ -1 2) 1)
+
+;; letrec https://github.com/zjhmale/Ntha/issues/1
+
+(let [ev? (λ n →
+            (match (λ n → (if (zero? n) false (ev? (dec n))))
+              (od? → (if (zero? n) true (od? (dec n))))))
+      od? (λ n →
+            (match (λ n → (if (zero? n) true (od? (dec n))))
+              (ev? → (if (zero? n) false (ev? (dec n))))))]
+  (begin (print (bool2str (ev? 11)))
+         (print (bool2str (ev? 12)))
+         (print (bool2str (od? 11)))
+         (print (bool2str (od? 12)))))
+
+(id : α → α)
+(ƒ id [a] a)
+
+(asserteq (id 3) 3)
+(asserteq (id true) true)
+
+(asserteq ((λ(x: α) : α → x) 3) 3)
+(asserteq ((λ(x: α) : α → x) true) true)
+
+(let id' (λ(x: α) : α → x))
+(asserteq (id' 3) 3)
+(asserteq (id' true) true)
+
+(foo : (x : Z | (> x 5)) → (z : Z | (> z 0)))
+(ƒ foo [x] (- x 5))
+
+(add : (x : Z | (≥ x 3)) → (y : Z | (≥ y 3)) → (z : Z | (≥ z 6)))
+(ƒ add [x y] (+ x y))
+
+(max : Z → Z → (z : Z | (∧ (≥ z x) (≥ z y))))
+(ƒ max [x y] (if (≤ x y) y x))
diff --git a/ntha.cabal b/ntha.cabal
--- a/ntha.cabal
+++ b/ntha.cabal
@@ -1,5 +1,5 @@
 name:                ntha
-version:             0.1.0
+version:             0.1.1
 synopsis:            A tiny statically typed functional programming language.
 description:         Check out <https://github.com/zjhmale/Ntha#readme the readme> for documentation.
 homepage:            https://github.com/zjhmale/ntha
@@ -17,7 +17,7 @@
     README.md
 data-files:
     lib/std.ntha
-
+    examples/misc.ntha
 
 library
   hs-source-dirs:      src
@@ -32,17 +32,29 @@
                      , Prologue
                      , Lexer
                      , Parser
+                     , Z3.Assertion
+                     , Z3.Class
+                     , Z3.Context
+                     , Z3.Encoding
+                     , Z3.Logic
   build-depends:       base >= 4.7 && < 5
                      , containers
                      , pretty
                      , monad-loops
                      , array
-                     , z3 >=4.4.1
-                     , z3-encoding
+                     , z3 >= 4.1.0
+                     , mtl >= 2.2 && < 2.3
+                   --, z3-encoding
   build-tools:         happy
                      , alex
   default-extensions:  TupleSections
                      , StandaloneDeriving
+                     , FlexibleInstances
+                     , FlexibleContexts
+                     , ScopedTypeVariables
+                     , MultiParamTypeClasses
+                     , RankNTypes
+                     , GADTs
   default-language:    Haskell2010
   ghc-options:         -Wall
 
diff --git a/src/Z3/Assertion.hs b/src/Z3/Assertion.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Assertion.hs
@@ -0,0 +1,63 @@
+-- |
+-- Assertions provided by libraries *for convenience*
+-- It is not hard-coded into Z3.Logic.Pred
+--
+
+module Z3.Assertion (Assertion(..)) where
+
+import Z3.Class
+import Z3.Encoding()
+import Z3.Monad
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+data Assertion where
+    -- | k is mapped to v in (m :: M.Map k v)
+    -- XXX: m should be any "term", too strong now
+    InMap    :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Assertion
+    -- | v is in s
+    -- XXX: s should be any "term", too strong now
+    InSet    :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Assertion
+    -- | All below are binary relationships
+    -- XXX: Should make sure v1 ~ v2, too weak now
+    Equal    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
+    LessE    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
+    GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
+    Less     :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
+    Greater  :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
+
+instance Z3Encoded Assertion where
+    encode (InMap k v m) = do
+        kTm <- encode k
+        vTm <- encode v
+        mTm <- encode m
+        lhs <- mkSelect mTm kTm
+        mkEq lhs vTm
+    encode (InSet e s) = do
+        eTm <- encode e
+        sTm <- encode s
+        lhs <- mkSelect sTm eTm
+        -- XXX: magic number
+        one <- (mkIntSort >>= mkInt 1)
+        mkEq one lhs
+    encode (Equal t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkEq a1 a2
+    encode (LessE t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkLe a1 a2
+    encode (GreaterE t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkGe a1 a2
+    encode (Less t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkLt a1 a2
+    encode (Greater t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkGt a1 a2
diff --git a/src/Z3/Class.hs b/src/Z3/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Class.hs
@@ -0,0 +1,223 @@
+-- |
+-- Type classes and built-in implementation for primitive Haskell types
+-- 
+
+module Z3.Class (
+    -- ** Types whose values are encodable to Z3 internal AST
+    Z3Encoded(..),
+    -- ** Types representable as Z3 Sort
+    -- XXX: Unsound now
+    -- XXX: Too flexible, can be used to encode Type ADT
+    Z3Sorted(..),
+    -- ** Type proxy helper, used with Z3Sorted
+    Z3Sort(..),
+    -- ** Types with reserved value for Z3 encoding use
+    -- XXX: Magic value for built-in types
+    Z3Reserved(..),
+    -- ** Monad which can be instantiated into a concrete context
+    SMT(..)
+) where
+
+import Z3.Monad
+import Z3.Logic
+
+import Control.Monad.Except
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+data Z3Sort a = Z3Sort
+
+class Z3Encoded a where
+    encode :: SMT m e => a -> m e AST
+
+-- | XXX: Unsound
+class Z3Sorted a where
+    -- | Map a value to Sort, the value should be a type-level thing
+    sort :: SMT m e => a -> m e Sort
+    sort _ = sortPhantom (Z3Sort :: Z3Sort a)
+
+    -- | Map a Haskell type to Sort
+    sortPhantom :: SMT m e => Z3Sort a -> m e Sort
+    sortPhantom _ = smtError "sort error"
+
+class Z3Encoded a => Z3Reserved a where
+    def :: a
+
+class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where
+    -- | Globally unique id
+    genFreshId :: m e Int
+
+    -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad
+    runSMT :: Z3Sorted ty => [(String, [(String, [(String, ty)])])] -> e -> m e a -> IO (Either String a)
+
+    -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort
+    bindQualified :: String -> AST -> Sort -> m e ()
+
+    -- | Get the above AST
+    -- FIXME: The context management need extra -- we need to make sure that old binding wouldn't be destoryed
+    -- XXX: We shouldn't expose a Map here. A fallible query interface is better
+    getQualifierCtx :: m e (M.Map String (AST, Sort))
+
+    -- | Get the preprocessed datatype context, a map from ADT's type name to its Z3 Sort
+    -- XXX: We shouldn't expose a Map here. A fallible query interface is better
+    getDataTypeCtx :: m e (M.Map String Sort)
+
+    -- | Get extra
+    getExtra :: m e e
+
+    -- | Set extra
+    modifyExtra :: (e -> e) -> m e ()
+
+    -- | User don't have to import throwError
+    smtError :: String -> m e a
+    smtError = throwError
+
+instance Z3Reserved Int where
+    def = -1 -- XXX: Magic number
+
+instance Z3Sorted Int where
+    sortPhantom _ = mkIntSort
+
+instance Z3Encoded Int where
+    encode i = mkIntSort >>= mkInt i
+
+instance Z3Reserved Double where
+    def = -1.0 -- XXX: Magic number
+
+instance Z3Sorted Double where
+    sortPhantom _ = mkRealSort
+
+instance Z3Encoded Double where
+    encode = mkRealNum
+
+instance Z3Reserved Bool where
+    def = False -- XXX: Magic number
+
+instance Z3Sorted Bool where
+    sortPhantom _ = mkBoolSort
+
+instance Z3Encoded Bool where
+    encode = mkBool
+
+-- The basic idea:
+-- For each (k, v), assert in Z3 that if we select k from array we will get
+-- the same value v
+-- HACK: to set a default value for rest fields (or else we always get the last asserted value
+--       as default, which is certainly not complying to finite map's definition), thus the
+--       user should guarantee that he/she will never never think this value as a vaid one,
+--       if not, he/she might get "a valid value mapped to a invalid key" semantics
+instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where
+    encode m = do
+        fid <- genFreshId
+        arrSort <- sort m
+        arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort
+        mapM_ (\(k, v) -> do
+            kast <- encode k
+            vast <- encode v
+            sel <- mkSelect arr kast
+            mkEq sel vast >>= assert) (M.toList m)
+        arrValueDef <- mkArrayDefault arr
+        vdef <- encode (def :: v)
+        mkEq arrValueDef vdef >>= assert
+        return arr
+
+instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where
+    sortPhantom _ = do
+        sk <- sortPhantom  (Z3Sort :: Z3Sort k)
+        sv <- sortPhantom  (Z3Sort :: Z3Sort v)
+        mkArraySort sk sv
+
+-- Basic idea:
+-- Set v =def= Map v {0, 1}
+-- Thank god, this is much more sound
+instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where
+    encode s = do
+        setSort <- sort s
+        fid <- genFreshId
+        arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort
+        mapM_ (\e -> do
+            ast <- encode e
+            sel <- mkSelect arr ast
+            one <- (mkIntSort >>= mkInt 1)
+            mkEq sel one >>= assert) (S.toList s)
+        arrValueDef <- mkArrayDefault arr
+        zero <- (mkIntSort >>= mkInt 0)
+        mkEq zero arrValueDef >>= assert
+        return arr
+
+instance Z3Sorted v => Z3Sorted (S.Set v) where
+    sortPhantom _ = do
+        sortElem <- sortPhantom (Z3Sort :: Z3Sort v)
+        intSort <- mkIntSort
+        mkArraySort sortElem intSort
+
+instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where
+    encode PTrue = mkTrue
+    encode PFalse = mkFalse
+    encode (PConj p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkAnd [a1, a2]
+
+    encode (PDisj p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkOr [a1, a2]
+
+    encode (PXor p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkXor a1 a2
+
+    encode (PNeg p) = encode p >>= mkNot
+
+    encode (PForAll x ty p) = do
+        sym <- mkStringSymbol x
+        xsort <- sort ty
+        -- "0" is de brujin idx for current binder
+        -- it is passed to Z3 which returns an intenal (idx :: AST)
+        -- This (idx :: AST) will be used to replace the variable
+        -- in the abstraction body when encountered, thus it is stored
+        -- in context by bindQualified we provide
+        -- XXX: we should save and restore qualifier context here
+        idx <- mkBound 0 xsort
+        local $ do
+            bindQualified x idx xsort
+            body <- encode p
+            -- The first [] is [Pattern], which is not really useful here
+            mkForall [] [sym] [xsort] body
+
+    encode (PExists x ty p) = do
+        sym <- mkStringSymbol x
+        xsort <- sort ty
+        idx <- mkBound 0 xsort
+        local $ do
+            bindQualified x idx xsort
+            a <- encode p
+            mkExists [] [sym] [xsort] a
+
+    -- HACK
+    encode (PExists2 x y ty p) = do
+        sym1 <- mkStringSymbol x
+        sym2 <- mkStringSymbol y
+        xsort <- sort ty
+        idx1 <- mkBound 0 xsort
+        idx2 <- mkBound 1 xsort
+        local $ do
+            bindQualified x idx1 xsort
+            bindQualified y idx2 xsort
+            a <- encode p
+            mkExists [] [sym1, sym2] [xsort, xsort] a
+
+    encode (PImpli p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkImplies a1 a2
+
+    encode (PIff p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkIff a1 a2
+
+    encode (PAssert a) = encode a
diff --git a/src/Z3/Context.hs b/src/Z3/Context.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Context.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- | A concrete context implement SMT provided *for convenience*
+
+module Z3.Context (Z3SMT) where
+
+import Z3.Monad
+import Z3.Class
+import Z3.Encoding
+
+import Control.Monad.State
+import Control.Monad.Except
+import qualified Data.Map as M
+
+data SMTContext e = SMTContext {
+    -- | Bind local variables introduced by qualifiers to de brujin index in Z3
+    _qualifierContext :: M.Map String (AST, Sort),
+    -- | From type name to Z3 sort
+    _datatypeCtx :: M.Map String Sort,
+    -- | Counter used to generate globally unique ID
+    _counter :: Int,
+    -- | Extra field reserved for extension
+    _extra :: e
+} deriving (Show, Eq)
+
+newtype Z3SMT e a = Z3SMT { unZ3SMT :: ExceptT String (StateT (SMTContext e) Z3) a }
+    deriving (Monad, Applicative, Functor, MonadState (SMTContext e), MonadIO, MonadError String)
+
+instance MonadZ3 (Z3SMT e) where
+  getSolver  = Z3SMT (lift (lift getSolver))
+  getContext = Z3SMT (lift (lift getContext))
+
+instance SMT Z3SMT e where
+    genFreshId = do
+        i <- _counter <$> get
+        modify (\ctx -> ctx { _counter = i + 1 })
+        return i
+
+    runSMT datatypes e smt = evalZ3With Nothing opts m
+        where
+            smt' = do
+                sorts <- mapM encodeDataType datatypes
+                let datatypeCtx = M.fromList (zip (map fst datatypes) sorts)
+                modify $ \ctx -> ctx { _datatypeCtx = datatypeCtx }
+                smt
+
+            -- XXX: not sure what does this option mean
+            opts = opt "MODEL" True
+            m = evalStateT (runExceptT (unZ3SMT smt'))
+                           (SMTContext M.empty M.empty 0 e)
+
+    bindQualified x idx s = modify $ \ctx ->
+            ctx { _qualifierContext = M.insert x (idx, s) (_qualifierContext ctx) }
+
+    getQualifierCtx = _qualifierContext <$> get
+
+    getDataTypeCtx = _datatypeCtx <$> get
+
+    getExtra = _extra <$> get
+
+    modifyExtra f = modify $ \ctx -> ctx { _extra = f (_extra ctx) }
diff --git a/src/Z3/Encoding.hs b/src/Z3/Encoding.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Encoding.hs
@@ -0,0 +1,52 @@
+-- |
+-- Prviding some Z3 encoding for certain language constructs
+-- Require a Class.SMT context to work
+
+module Z3.Encoding (
+  -- ** Heterogenous list, a hack to encode different "term" into a list
+  -- Used to encode function argument list
+  HeteroList(..),
+  -- ** encode function application
+  encodeApp,
+  -- ** encode datatype definition
+  encodeDataType
+) where
+
+import Z3.Class
+import Z3.Monad hiding (mkMap, App)
+
+data HeteroList where
+    Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList
+    Nil :: HeteroList
+
+instance Eq HeteroList where
+  Nil == Nil = True
+  Cons _ h1 == Cons _ h2 = h1 == h2
+  _ == _ = False
+
+mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]
+mapH _ Nil = []
+mapH f (Cons a l) = f a : mapH f l
+
+encodeApp :: SMT m e => String -> HeteroList -> Sort -> m e AST
+encodeApp fname args retSort = do
+    paramSorts <- sequence $ mapH sort args
+    sym <- mkStringSymbol fname
+    decl <- mkFuncDecl sym paramSorts retSort
+    argASTs <- sequence $ mapH encode args
+    mkApp decl argASTs
+
+encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort
+encodeDataType (tyName, alts) = do
+    constrs <- mapM (\(consName, fields) -> do
+                        consSym <- mkStringSymbol consName
+                        -- recognizer. e.g. is_None None = True, is_None (Some _) = False
+                        recogSym <- mkStringSymbol ("is_" ++ consName)
+                        flds <- flip mapM fields $ \(fldName, fldTy) -> do
+                            symFld <- mkStringSymbol fldName
+                            s <- sort fldTy
+                            return (symFld, Just s, -1) -- XXX: non-rec
+                        mkConstructor consSym recogSym flds
+                    ) alts
+    sym <- mkStringSymbol tyName
+    mkDatatype sym constrs
diff --git a/src/Z3/Logic.hs b/src/Z3/Logic.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Logic.hs
@@ -0,0 +1,18 @@
+-- | Predicates
+
+module Z3.Logic (Pred(..)) where
+
+data Pred t ty a where
+    PTrue   :: Pred t ty a
+    PFalse  :: Pred t ty a
+    PConj   :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PDisj   :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PXor    :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PNeg    :: Pred t ty a -> Pred t ty a
+    PForAll :: String -> ty -> Pred t ty a -> Pred t ty a
+    PExists :: String -> ty -> Pred t ty a -> Pred t ty a
+    PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a
+    PImpli  :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PIff    :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PAssert :: a -> Pred t ty a
+    deriving (Show)
diff --git a/test/EvalSpec.hs b/test/EvalSpec.hs
--- a/test/EvalSpec.hs
+++ b/test/EvalSpec.hs
@@ -11,12 +11,12 @@
 
 runEvalSpecCases :: [(Expr, Maybe Value)] -> IO ()
 runEvalSpecCases exprExpects = do
-    let (_, vals, expects) = foldl (\(env, vals, expects) (expr, expect) → let (env', val) = eval expr env
+    let (_, vals', expects') = foldl (\(env, vals, expects) (expr, expect) → let (env', val) = eval expr env
                                                                            in case expect of
                                                                                 Just e -> (env', vals ++ [val], expects ++ [e])
                                                                                 Nothing -> (env', vals, expects))
                                    (builtins, [], []) exprExpects
-    (map (PP.text . show) vals) `shouldBe` map (PP.text . show) expects
+    (map (PP.text . show) vals') `shouldBe` map (PP.text . show) expects'
 
 spec :: Spec
 spec = describe "evaluation test" $ do
@@ -104,7 +104,7 @@
           let res0 = EDestructLetBinding (IdPattern "res0") [] [EApp (EApp (EVar "g") $ ENum 3) $ ENum 3]
           let f = EDestructLetBinding (IdPattern "f") [] [ELambda [Named "x" (Just intT), Named "y" (Just intT), Named "z" (Just intT)] (Just intT) [EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "x") $ EVar "y")) $ EVar "z"]]
           let res1 = EDestructLetBinding (IdPattern "res1") [] [EApp (EApp (EApp (EVar "f") $ ENum 8) $ ENum 2) $ ENum 3]
-          let id = EDestructLetBinding (IdPattern "id") [] [ELambda [Named "x" Nothing] Nothing [EVar "x"]]
+          let idfn = EDestructLetBinding (IdPattern "id") [] [ELambda [Named "x" Nothing] Nothing [EVar "x"]]
           let res2 = EDestructLetBinding (IdPattern "res2") [] [EApp (EVar "id") $ ENum 3]
           let res3 = EDestructLetBinding (IdPattern "res3") [] [EApp (EVar "id") $ EBool True]
           let idpair = ELetBinding (IdPattern "id") (ELambda [Named "x" Nothing] Nothing [EVar "x"]) [(ETuple [EApp (EVar "id") (ENum 3), EApp (EVar "id") (EBool True)])]
@@ -117,7 +117,7 @@
                             (res0, Just $ VNum 6),
                             (f, Nothing),
                             (res1, Just $ VNum 13),
-                            (id, Nothing),
+                            (idfn, Nothing),
                             (res2, Just $ VNum 3),
                             (res3, Just $ VBool True),
                             (idpair, Just $ VTuple [VNum 3, VBool True]),
@@ -138,7 +138,7 @@
                                                                                                                                     Case (TConPattern "Cons" [IdPattern "x", TConPattern "Cons" [IdPattern "y", IdPattern "t"]]) [EApp (EVar "penultimate") (EVar "t")]]]]
           let res7 = EDestructLetBinding (IdPattern "res7") [] [EApp (EVar "penultimate") (EList [ENum 1, ENum 2, ENum 3])]
           let res8 = EDestructLetBinding (IdPattern "res7") [] [EApp (EVar "penultimate") (EList [ENum 1, ENum 2, ENum 3, ENum 4])]
-          let map = EDestructLetBinding (IdPattern "map") [IdPattern "f", IdPattern "l"] [EPatternMatching (EVar "l") [Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "Cons") $ EApp (EVar "f") $ EVar "h") $ EApp (EApp (EVar "map") $ EVar "f") $ EVar "t"],Case (TConPattern "Nil" []) [EVar "Nil"]]]
+          let mapfn = EDestructLetBinding (IdPattern "map") [IdPattern "f", IdPattern "l"] [EPatternMatching (EVar "l") [Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "Cons") $ EApp (EVar "f") $ EVar "h") $ EApp (EApp (EVar "map") $ EVar "f") $ EVar "t"],Case (TConPattern "Nil" []) [EVar "Nil"]]]
           let map2 = EDestructLetBinding (IdPattern "map2") [IdPattern "f", IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [EList []],Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "Cons") $ EApp (EVar "f") $ EVar "h") $ EApp (EApp (EVar "map2") $ EVar "f") $ EVar "t"]]]
           let l = EDestructLetBinding (IdPattern "l") [] [EList [ENum 1, ENum 2, ENum 3]]
           let l3 = EDestructLetBinding (IdPattern "l3") [] [EApp (EApp (EVar "map") $ ELambda [Named "x" Nothing] Nothing [EApp (EApp (EVar "=") $ EApp (EApp (EVar "%") $ EVar "x") $ ENum 2) $ ENum 0]) $ EVar "l"]
@@ -169,7 +169,7 @@
                             (penultimate, Nothing),
                             (res7, Just $ VNum 0),
                             (res8, Just $ VNum 3),
-                            (map, Nothing),
+                            (mapfn, Nothing),
                             (map2, Nothing),
                             (l, Just $ cons (VNum 1) (cons (VNum 2) (cons (VNum 3) nil))),
                             (l3, Just $ cons (VBool False) (cons (VBool True) (cons (VBool False) nil))),