diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -9,13 +9,13 @@
 whether, under a given sequence of definitions,
 a particular term _reduces to_ to another.
 
-## Online Demo 
+## Online Demo
 
 You can try `elsa` online at [this link](http://goto.ucsd.edu:8095/index.html)
 
-## Install 
+## Install
 
-You can locally build and run `elsa` by 
+You can locally build and run `elsa` by
 
 1. Installing [stack](https://www.haskellstack.org)
 2. Cloning this repo
@@ -23,14 +23,14 @@
 
 That is, to say
 
-```bash 
+```bash
 $ curl -sSL https://get.haskellstack.org/ | sh
 $ git clone https://github.com/ucsd-progsys/elsa.git
-$ cd elsa 
+$ cd elsa
 $ stack install
 ```
 
-## Overview 
+## Overview
 
 `elsa` programs look like:
 
@@ -41,9 +41,14 @@
 
 eval id_zero :
   id zero
-  =d> (\x -> x) (\f x -> x)
-  =b> (\f x -> x)
-  =d> zero
+  =d> (\x -> x) (\f x -> x)   -- expand definitions
+  =a> (\z -> z) (\f x -> x)   -- alpha rename
+  =b> (\f x -> x)             -- beta reduce
+  =d> zero                    -- expand definitions
+
+eval id_zero_tr :
+  id zero  
+  =*> zero                    -- transitive reductions
 ```
 
 When you run `elsa` on the above, you should get the following output:
@@ -51,7 +56,7 @@
 ```bash
 $ elsa ex1.lc
 
-OK id_zero.
+OK id_zero, id_zero_tr.
 ```
 
 ## Partial Evaluation
@@ -97,7 +102,7 @@
   =d> (\n f x -> f (n f x)) (\f x -> f x)
   =b> \f x -> f ((\f x -> f x) f x)
   =b> \f x -> f ((\x -> f x) x)
-  =b> \f x -> f (f x)                 -- beta-reduce the above 
+  =b> \f x -> f (f x)                 -- beta-reduce the above
   =d> two                             -- optional
 ```
 
@@ -163,6 +168,8 @@
 <step>      ::= =a>   -- alpha equivalence
                 =b>   -- beta  equivalence
                 =d>   -- def   equivalence
+                =*>   -- trans equivalence
+                =~>   -- normalizes to
 ```
 
 
@@ -178,3 +185,9 @@
 * `t =a> t'` is valid if `t` and `t'` are equivalent up to **alpha-renaming**,
 * `t =b> t'` is valid if `t` **beta-reduces** to `t'` in a single step,
 * `t =d> t'` is valid if `t` and `t'` are identical after **let-expansion**.
+* `t =*> t'` is valid if `t` and `t'` are in the reflexive, transitive closure
+             of the union of the above three relations.
+* `t =~> t'` is valid if `t` [normalizes to][normalform] `t'`.
+
+[normalform]: http://dl.acm.org/citation.cfm?id=860276
+[normalform-pdf]: http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf
diff --git a/elsa.cabal b/elsa.cabal
--- a/elsa.cabal
+++ b/elsa.cabal
@@ -1,7 +1,7 @@
 name:                elsa
-version:             0.1.0.0
+version:             0.1.0.1
 synopsis:            A tiny language for understanding the lambda-calculus
-description:         elsa is a small proof checker for verifying sequences of 
+description:         elsa is a small proof checker for verifying sequences of
                      reductions of lambda-calculus terms. The goal is to help
                      students build up intuition about lambda-terms, alpha-equivalence,
                      beta-reduction, and in general, the notion of computation
@@ -11,7 +11,7 @@
 author:              Ranjit Jhala
 maintainer:          jhala@cs.ucsd.edu
 category:            Language
-Homepage:            http://github.com/ucsd-progsys/elsa 
+Homepage:            http://github.com/ucsd-progsys/elsa
 build-type:          Simple
 extra-source-files:  README.md
 cabal-version:       >=1.10
@@ -21,27 +21,28 @@
   Location:    https://github.com/ucsd-progsys/elsa/
 
 Library
-  ghc-options:        -W 
-  exposed-modules:    Language.Elsa.Types,
+  ghc-options:        -W
+  exposed-modules:    Language.Elsa
+                      Language.Elsa.Types,
                       Language.Elsa.Eval,
                       Language.Elsa.Parser,
                       Language.Elsa.Runner
 
   Default-Extensions: OverloadedStrings
 
-  -- other-extensions:
   build-depends:       base >= 4 && < 5,
                        array,
                        mtl,
                        megaparsec,
-                       containers,
+                       hashable,
+                       unordered-containers,
                        directory,
                        filepath,
+                       dequeue,
                        json
 
   hs-source-dirs:      src
   default-language:    Haskell2010
---  build-tools:         alex, happy
   other-modules:       Language.Elsa.UX,
                        Language.Elsa.Utils
 
diff --git a/src/Language/Elsa.hs b/src/Language/Elsa.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Elsa.hs
@@ -0,0 +1,8 @@
+--  Re-export library
+
+module Language.Elsa ( module X ) where
+
+import Language.Elsa.Types  as X
+import Language.Elsa.Parser as X
+import Language.Elsa.Eval   as X
+import Language.Elsa.Runner as X
diff --git a/src/Language/Elsa/Eval.hs b/src/Language/Elsa/Eval.hs
--- a/src/Language/Elsa/Eval.hs
+++ b/src/Language/Elsa/Eval.hs
@@ -1,21 +1,32 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Language.Elsa.Eval where
+module Language.Elsa.Eval (elsa, elsaOn) where
 
-import qualified Data.Map  as M
-import qualified Data.Set  as S
+import qualified Data.HashMap.Strict  as M
+import qualified Data.HashSet         as S
+import qualified Data.List            as L
 import           Control.Monad.State
-import           Data.Maybe (maybeToList)
+import           Data.Maybe           (mapMaybe, isJust, maybeToList)
 import           Language.Elsa.Types
-import           Language.Elsa.Utils (fromEither)
+import           Language.Elsa.Utils  (qPushes, qInit, qPop, fromEither)
 
+
 --------------------------------------------------------------------------------
 elsa :: Elsa a -> [Result a]
 --------------------------------------------------------------------------------
-elsa p = case mkEnv (defns p) of
-           Left err -> [err]
-           Right g  -> [result g e | e <- evals p]
+elsa = elsaOn (const True)
 
+--------------------------------------------------------------------------------
+elsaOn :: (Id -> Bool) -> Elsa a -> [Result a]
+--------------------------------------------------------------------------------
+elsaOn cond p =
+  case mkEnv (defns p) of
+    Left err -> [err]
+    Right g  -> [result g e | e <- evals p, check e ]
+  where
+    check = cond . bindId . evName
+
+
 result :: Env a -> Eval a -> Result a
 result g e = fromEither (eval g e)
 
@@ -32,7 +43,7 @@
 
 --------------------------------------------------------------------------------
 type CheckM a b = Either (Result a) b
-type Env a      = M.Map Id (Expr a)
+type Env a      = M.HashMap Id (Expr a)
 --------------------------------------------------------------------------------
 
 --------------------------------------------------------------------------------
@@ -53,9 +64,34 @@
 isEq :: Eqn a -> Env a -> Expr a -> Expr a -> Bool
 isEq (AlphEq _) = isAlphEq
 isEq (BetaEq _) = isBetaEq
+isEq (UnBeta _) = isUnBeta
 isEq (DefnEq _) = isDefnEq
+isEq (TrnsEq _) = isTrnsEq
+isEq (UnTrEq _) = isUnTrEq
+isEq (NormEq _) = isNormEq
 
+
 --------------------------------------------------------------------------------
+-- | Transitive Reachability
+--------------------------------------------------------------------------------
+isTrnsEq :: Env a -> Expr a -> Expr a -> Bool
+isTrnsEq g e1 e2 = isJust (findTrans (isEquiv g e2) (canon g e1))
+
+isUnTrEq :: Env a -> Expr a -> Expr a -> Bool
+isUnTrEq g e1 e2 = isTrnsEq g e2 e1
+
+findTrans :: (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
+findTrans p e = go S.empty (qInit e)
+  where
+    go seen q = do
+      (e, q') <- qPop q
+      if S.member e seen
+        then go seen q'
+        else if p e
+             then return e
+             else go (S.insert e seen) (qPushes q (betas e))
+
+--------------------------------------------------------------------------------
 -- | Definition Equivalence
 --------------------------------------------------------------------------------
 isDefnEq :: Env a -> Expr a -> Expr a -> Bool
@@ -68,11 +104,14 @@
 isAlphEq _ e1 e2 = alphaNormal e1 == alphaNormal e2
 
 alphaNormal :: Expr a -> Expr a
-alphaNormal e = evalState (normalize M.empty e) 0
+alphaNormal = alphaShift 0
 
+alphaShift :: Int -> Expr a -> Expr a
+alphaShift n e = evalState (normalize M.empty e) n
+
 type AlphaM a = State Int a
 
-normalize :: M.Map Id Id -> Expr a -> AlphaM (Expr a)
+normalize :: M.HashMap Id Id -> Expr a -> AlphaM (Expr a)
 normalize g (EVar x z) =
   return (EVar (rename g x) z)
 
@@ -87,21 +126,35 @@
   e'    <- normalize g' e
   return (ELam (Bind y z1) e' z2)
 
-rename :: M.Map Id Id -> Id -> Id
-rename g x = M.findWithDefault x x g
+rename :: M.HashMap Id Id -> Id -> Id
+rename g x = M.lookupDefault x x g
 
 fresh :: AlphaM Id
 fresh = do
   n <- get
   put (n + 1)
-  return ("$x" ++ show n)
+  return (newAId n)
 
+newAId :: Int -> Id
+newAId n = aId ++ show n
+
+isAId :: Id -> Maybe Int
+isAId x
+  | L.isPrefixOf aId x = Just . read . drop 2 $ x
+  | otherwise          = Nothing
+
+aId :: String
+aId = "$x"
+
 --------------------------------------------------------------------------------
 -- | Beta Reduction
 --------------------------------------------------------------------------------
 isBetaEq :: Env a -> Expr a -> Expr a -> Bool
-isBetaEq _ e1 e2 = or [ e1' == e2 | e1' <- betas e1]
+isBetaEq _ e1 e2 = or [ e1' == e2  | e1' <- betas e1 ]
 
+isUnBeta :: Env a -> Expr a -> Expr a -> Bool
+isUnBeta g e1 e2 = isBetaEq g e2 e1
+
 isNormal :: Env a -> Expr a -> Bool
 isNormal g = null . betas . (`subst` g)
 
@@ -133,30 +186,69 @@
     go bs (ELam b e1  l) = do e1' <- go (b:bs) e1
                               Just (ELam b e1' l)
 
-isIn :: Bind a -> S.Set Id -> Bool
+isIn :: Bind a -> S.HashSet Id -> Bool
 isIn = S.member . bindId
 
 --------------------------------------------------------------------------------
--- | Free Variables and Substitution
+-- | Evaluation to Normal Form
+--   http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf
 --------------------------------------------------------------------------------
-freeVars :: Expr a -> S.Set Id
+isNormEq :: Env a -> Expr a -> Expr a -> Bool
+isNormEq g e1 e2 = isEquiv g e1' e2
+  where
+    e1'          = evalNO (canon g e1)
+
+-- | normal-order reduction
+evalNO :: Expr a -> Expr a
+evalNO e@(EVar {})    = e
+evalNO (ELam b e l)   = ELam b (evalNO e) l
+evalNO (EApp e1 e2 l) = case evalCBN e1 of
+                          ELam b e1' _ -> evalNO (bSubst e1' (bindId b) e2)
+                          e1'          -> EApp (evalNO e1') (evalNO e2) l
+
+-- | call-by-name reduction
+evalCBN :: Expr a -> Expr a
+evalCBN e@(EVar {}) = e
+evalCBN e@(ELam {}) = e
+evalCBN (EApp e1 e2 l) = case evalCBN e1 of
+                          ELam b e1' _ -> evalCBN (bSubst e1' (bindId b) e2)
+                          e1'          -> EApp e1' e2 l
+
+-- | Force alpha-renaming to ensure capture avoiding subst
+bSubst :: Expr a -> Id -> Expr a -> Expr a
+bSubst e x e' = subst e (M.singleton x e'')
+  where
+    e''       = alphaShift n e'
+    n         = 1 + maximum (0 : mapMaybe isAId vs)
+    vs        = S.toList (freeVars e')
+
+--------------------------------------------------------------------------------
+-- | General Helpers
+--------------------------------------------------------------------------------
+freeVars :: Expr a -> S.HashSet Id
 freeVars = S.fromList . M.keys . freeVars'
 
-freeVars' :: Expr a -> M.Map Id a
+freeVars' :: Expr a -> M.HashMap Id a
 freeVars' (EVar x l)    = M.singleton x l
 freeVars' (ELam b e _)  = M.delete (bindId b)    (freeVars' e)
 freeVars' (EApp e e' _) = M.union  (freeVars' e) (freeVars' e')
 
 subst :: Expr a -> Env a -> Expr a
-subst e@(EVar v _)   su = M.findWithDefault e v su
+subst e@(EVar v _)   su = M.lookupDefault e v su
 subst (EApp e1 e2 z) su = EApp (subst e1 su) (subst e2 su) z
 subst (ELam b e z)   su = ELam b (subst e su') z
   where
     su'                 = M.delete (bindId b) su
 
+canon :: Env a -> Expr a -> Expr  a
+canon g = alphaNormal . (`subst` g)
+
+isEquiv :: Env a -> Expr a -> Expr a -> Bool
+isEquiv g e1 e2 = isAlphEq g (subst e1 g) (subst e2 g)
 --------------------------------------------------------------------------------
 -- | Error Cases
 --------------------------------------------------------------------------------
+
 errInvalid :: Bind a -> Expr a -> Eqn a -> Expr a -> Result a
 errInvalid b _ eqn _ = Invalid b (tag eqn)
 
diff --git a/src/Language/Elsa/Parser.hs b/src/Language/Elsa/Parser.hs
--- a/src/Language/Elsa/Parser.hs
+++ b/src/Language/Elsa/Parser.hs
@@ -1,4 +1,7 @@
-module Language.Elsa.Parser ( parse, parseFile ) where
+module Language.Elsa.Parser
+  ( parse
+  , parseFile
+  ) where
 
 import           Control.Monad (void)
 import           Text.Megaparsec hiding (parse)
@@ -137,10 +140,11 @@
 eqn :: Parser SEqn
 eqn =  try (withSpan' (symbol "=a>" >> return AlphEq))
    <|> try (withSpan' (symbol "=b>" >> return BetaEq))
-   <|>     (withSpan' (symbol "=d>" >> return DefnEq))
-
--- expr :: Parser SExpr
--- expr = makeExprParser expr0 []
+   <|> try (withSpan' (symbol "<b=" >> return UnBeta))
+   <|> try (withSpan' (symbol "=d>" >> return DefnEq))
+   <|> try (withSpan' (symbol "=*>" >> return TrnsEq))
+   <|> try (withSpan' (symbol "<*=" >> return UnTrEq))
+   <|>     (withSpan' (symbol "=~>" >> return NormEq))
 
 expr :: Parser SExpr
 expr =  try lamExpr
diff --git a/src/Language/Elsa/Runner.hs b/src/Language/Elsa/Runner.hs
--- a/src/Language/Elsa/Runner.hs
+++ b/src/Language/Elsa/Runner.hs
@@ -1,21 +1,24 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 
-module Language.Elsa.Runner where
+module Language.Elsa.Runner
+  ( topMain
+  , runElsa
+  , runElsaId
+  ) where
 
 import Data.List            (intercalate)
 import Data.Maybe           (mapMaybe)
-import Control.Monad        (when)
+import Control.Monad        (when, void)
 import Control.Exception
 import System.IO
 import System.Exit
 import System.Environment   (getArgs)
-import System.FilePath      -- (takeDirectory, takeFileName)
-import System.Directory     -- (takeDirectory, takeFileName)
-import Language.Elsa.Parser (parse)
-import Language.Elsa.Types  (successes, resultError)
+import System.FilePath
+import System.Directory
+import Language.Elsa.Parser
+import Language.Elsa.Types
 import Language.Elsa.UX
-import Language.Elsa.Eval   (elsa)
-
+import Language.Elsa.Eval
 
 topMain:: IO ()
 topMain = do
@@ -45,8 +48,8 @@
 
 runElsa :: Mode -> FilePath -> Text -> IO ()
 runElsa mode f s = do
-  let rs  = elsa (parse f s)
-  let es  = mapMaybe resultError rs
+  let rs = elsa (parse f s)
+  let es = mapMaybe resultError rs
   when (null es && mode == Cmdline) (putStrLn (okMessage rs))
   exitErrors mode f es
 
@@ -60,3 +63,16 @@
     ["--server", f] -> return (Server,  f)
     [f]             -> return (Cmdline, f)
     _               -> error "Please run with a single file as input"
+
+
+--------------------------------------------------------------------------------
+runElsaId :: FilePath -> Id -> IO (Maybe (Result ()))
+--------------------------------------------------------------------------------
+runElsaId f x = ((`runElsa1` x) <$> parseFile f)
+                  `catch`
+                     (\(_ :: [UserError]) -> return Nothing)
+
+runElsa1 :: Elsa a -> Id -> Maybe (Result ())
+runElsa1 p x = case elsaOn (== x) p of
+                 [r] -> Just (void r)
+                 _   -> Nothing
diff --git a/src/Language/Elsa/Types.hs b/src/Language/Elsa/Types.hs
--- a/src/Language/Elsa/Types.hs
+++ b/src/Language/Elsa/Types.hs
@@ -1,33 +1,37 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveGeneric     #-}
+{-# LANGUAGE DeriveFunctor     #-}
 
 module Language.Elsa.Types where
 
+import           GHC.Generics
 import           Text.Printf (printf)
 import           Data.Monoid
 import           Language.Elsa.UX
 import           Data.Maybe (mapMaybe)
-
-type Id    = String
-
-type SElsa = Elsa SourceSpan
-type SDefn = Defn SourceSpan
-type SExpr = Expr SourceSpan
-type SEval = Eval SourceSpan
-type SStep = Step SourceSpan
-type SBind = Bind SourceSpan
-type SEqn  = Eqn  SourceSpan
+import           Data.Hashable
 
+type Id      = String
+type SElsa   = Elsa SourceSpan
+type SDefn   = Defn SourceSpan
+type SExpr   = Expr SourceSpan
+type SEval   = Eval SourceSpan
+type SStep   = Step SourceSpan
+type SBind   = Bind SourceSpan
+type SEqn    = Eqn  SourceSpan
+type SResult = Result SourceSpan
 
 --------------------------------------------------------------------------------
 -- | Result
 --------------------------------------------------------------------------------
+
 data Result a
   = OK      (Bind a)
   | Partial (Bind a)    a
   | Invalid (Bind a)    a
   | Unbound (Bind a) Id a
-  deriving (Eq, Show)
+  deriving (Eq, Show, Functor)
 
 failures :: [Result a] -> [Id]
 failures = mapMaybe go
@@ -55,7 +59,6 @@
 --------------------------------------------------------------------------------
 -- | Programs
 --------------------------------------------------------------------------------
-
 data Elsa a = Elsa
   { defns :: [Defn a]
   , evals :: [Eval a]
@@ -80,28 +83,54 @@
 data Eqn a
   = AlphEq a
   | BetaEq a
+  | UnBeta a
   | DefnEq a
+  | TrnsEq a
+  | UnTrEq a
+  | NormEq a
   deriving (Eq, Show)
 
 data Bind a
   = Bind Id a
-  deriving (Show)
+  deriving (Show, Functor)
 
 data Expr a
   = EVar Id                  a
   | ELam !(Bind a) !(Expr a) a
   | EApp !(Expr a) !(Expr a) a
-  deriving (Show)
+--  deriving (Show)
 
+instance Show (Expr a) where
+  show = pprint
+
 instance Eq (Bind a) where
   b1 == b2 = bindId b1 == bindId b2
 
+-- instance Eq (Expr a) where
+  -- (EVar x _)      == (EVar y _)      = x == y
+  -- (ELam b1 e1 _)  == (ELam b2 e2 _ ) = b1 == b2 && e1  == e2
+  -- (EApp e1 e1' _) == (EApp e2 e2' _) = e1 == e2 && e1' == e2'
+  -- _               == _               = False
+
+data RExpr
+  = RVar Id
+  | RLam Id    RExpr
+  | RApp RExpr RExpr
+  deriving (Eq, Generic)
+
+rExpr :: Expr a -> RExpr
+rExpr (EVar x _)    = RVar x
+rExpr (ELam b e  _) = RLam (bindId b) (rExpr e )
+rExpr (EApp e e' _) = RApp (rExpr  e) (rExpr e')
+
 instance Eq (Expr a) where
-  (EVar x _)      == (EVar y _)      = x == y
-  (ELam b1 e1 _)  == (ELam b2 e2 _ ) = b1 == b2 && e1  == e2
-  (EApp e1 e1' _) == (EApp e2 e2' _) = e1 == e2 && e1' == e2'
-  _               == _               = False
+  e1 == e2 = rExpr e1 == rExpr e2
 
+instance Hashable RExpr
+
+instance Hashable (Expr a) where
+  hashWithSalt i = hashWithSalt i . rExpr
+
 -------------------------------------------------------------------------------------
 -- | Pretty Printing
 -------------------------------------------------------------------------------------
@@ -140,7 +169,11 @@
 instance Tagged Eqn where
   tag (AlphEq x) = x
   tag (BetaEq x) = x
+  tag (UnBeta x) = x
   tag (DefnEq x) = x
+  tag (TrnsEq x) = x
+  tag (UnTrEq x) = x
+  tag (NormEq x) = x
 
 instance Tagged Bind where
   tag (Bind _   x) = x
diff --git a/src/Language/Elsa/Utils.hs b/src/Language/Elsa/Utils.hs
--- a/src/Language/Elsa/Utils.hs
+++ b/src/Language/Elsa/Utils.hs
@@ -1,7 +1,9 @@
 module Language.Elsa.Utils where
 
-import qualified Data.Map  as M
-import qualified Data.List as L
+import qualified Data.HashMap.Strict as M
+import qualified Data.List           as L
+import qualified Data.Dequeue        as Q
+import           Data.Hashable
 import           Data.Monoid
 import           Data.Char (isSpace)
 import           Control.Exception
@@ -10,13 +12,13 @@
 import           System.FilePath
 import           Debug.Trace (trace)
 
-groupBy :: (Ord k) => (a -> k) -> [a] -> [(k, [a])]
+groupBy :: (Eq k, Hashable k) => (a -> k) -> [a] -> [(k, [a])]
 groupBy f = M.toList . L.foldl' (\m x -> inserts (f x) x m) M.empty
 
-inserts :: (Ord k) => k -> v -> M.Map k [v] -> M.Map k [v]
-inserts k v m = M.insert k (v : M.findWithDefault [] k m) m
+inserts :: (Eq k, Hashable k) => k -> v -> M.HashMap k [v] -> M.HashMap k [v]
+inserts k v m = M.insert k (v : M.lookupDefault [] k m) m
 
-dupBy :: (Ord k) => (a -> k) -> [a] -> [[a]]
+dupBy :: (Eq k, Hashable k) => (a -> k) -> [a] -> [[a]]
 dupBy f xs = [ xs' | (_, xs') <- groupBy f xs, 2 <= length xs' ]
 
 trim :: String -> String
@@ -46,7 +48,26 @@
   = take (i2 - i1 + 1)
   . drop (i1 - 1)
 
-
 fromEither :: Either a a -> a
-fromEither (Left x)  = x 
+fromEither (Left x)  = x
 fromEither (Right x) = x
+
+--------------------------------------------------------------------------------
+-- | Queue ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+newtype Queue a = Q (Q.BankersDequeue a)
+
+qEmpty :: Queue a
+qEmpty = Q Q.empty
+
+qInit :: a -> Queue a
+qInit x = qPushes qEmpty [x]
+
+qPushes :: Queue a -> [a] -> Queue a
+qPushes (Q q) xs = Q (L.foldl' Q.pushFront q xs)
+
+qPop :: Queue a -> Maybe (a, Queue a)
+qPop (Q q) = case Q.popBack q of
+               Nothing      -> Nothing
+               Just (x, q') -> Just (x, Q q')