diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,5 +1,5 @@
 name:                liquid-fixpoint
-version:             0.7.0.5
+version:             0.7.0.6
 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
diff --git a/src/Language/Fixpoint/Minimize.hs b/src/Language/Fixpoint/Minimize.hs
--- a/src/Language/Fixpoint/Minimize.hs
+++ b/src/Language/Fixpoint/Minimize.hs
@@ -13,7 +13,6 @@
 import           Control.Monad                      (filterM)
 import           Language.Fixpoint.Types.Visitor    (mapKVars)
 import           Language.Fixpoint.Types.Config     (Config (..), queryFile)
-import           Language.Fixpoint.Types.Errors
 import           Language.Fixpoint.Misc             (safeHead)
 import           Language.Fixpoint.Utils.Files      hiding (Result)
 import           Language.Fixpoint.Graph
@@ -116,10 +115,6 @@
 ---------------------------------------------------------------------------
 -- Helper functions
 ---------------------------------------------------------------------------
-isSafe :: Result a -> Bool
-isSafe (Result Safe _ _) = True
-isSafe _                 = False
-
 addExt :: Ext -> Config -> Config
 addExt ext cfg = cfg { srcFile = queryFile ext cfg }
 
diff --git a/src/Language/Fixpoint/Misc.hs b/src/Language/Fixpoint/Misc.hs
--- a/src/Language/Fixpoint/Misc.hs
+++ b/src/Language/Fixpoint/Misc.hs
@@ -399,6 +399,11 @@
 powerset :: [a] -> [[a]]
 powerset xs = filterM (const [False, True]) xs
 
+(=>>) :: Monad m => m b -> (b -> m a) -> m b
+(=>>) m f = m >>= (\x -> f x >> return x)
+
+(<<=) :: Monad m => (b -> m a) -> m b -> m b
+(<<=) = flip (=>>)
 
 (<$$>) ::  (Monad m) => (a -> m b) -> [a] -> m [b]
 _ <$$> []           = return []
diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs
--- a/src/Language/Fixpoint/Parse.hs
+++ b/src/Language/Fixpoint/Parse.hs
@@ -158,6 +158,7 @@
 
   -- reserved words used in liquid haskell
   , "forall"
+  , "coerce"
   , "exists"
   , "module"
   , "spec"
@@ -195,6 +196,7 @@
   , "type"
   , "using"
   , "with"
+  , "in"
   ]
 
 reservedOpNames :: [String]
@@ -351,6 +353,7 @@
   =  trueP
  <|> falseP
  <|> (fastIfP EIte exprP)
+ <|> (coerceP exprP)
  <|> (ESym <$> symconstP)
  <|> (ECon <$> constantP)
  <|> (reservedOp "_|_" >> return EBot)
@@ -383,6 +386,15 @@
        b2 <- bodyP
        return $ f p b1 b2
 
+coerceP :: Parser Expr -> Parser Expr
+coerceP p = do
+  reserved "coerce"
+  (s, t) <- parens (pairP sortP (reservedOp "~") sortP)
+  e      <- p
+  return $ ECoerc s t e
+
+
+
 {-
 qmIfP f bodyP
   = parens $ do
@@ -694,13 +706,14 @@
 qualifierP tP = do
   pos    <- getPosition
   n      <- upperIdP
-  params <- parens $ sepBy1 (sortBindP tP) comma
+  params <- parens $ sepBy1 (symBindP tP) comma
   _      <- colon
   body   <- predP
   return  $ mkQual n params body pos
-  where
-    sortBindP = pairP symbolP colon
 
+symBindP :: Parser a -> Parser (Symbol, a)
+symBindP = pairP symbolP colon
+
 pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
 pairP xP sepP yP = (,) <$> xP <* sepP <*> yP
 
@@ -714,7 +727,12 @@
 ---------------------------------------------------------------------
 
 defineP :: Parser Equation
-defineP = Equ <$> symbolP <*> many symbolP <*> (reserved "=" >> exprP)
+defineP = do
+  name   <- symbolP
+  params <- parens        $ sepBy (symBindP sortP) comma
+  sort   <- colon        *> sortP
+  body   <- reserved "=" *> predP
+  return  $ mkEquation name params body sort
 
 matchP :: Parser Rewrite
 matchP = SMeasure <$> symbolP <*> symbolP <*> many symbolP <*> (reserved "=" >> exprP)
diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs
--- a/src/Language/Fixpoint/Smt/Interface.hs
+++ b/src/Language/Fixpoint/Smt/Interface.hs
@@ -80,6 +80,7 @@
 import           Data.Char
 import qualified Data.HashMap.Strict      as M
 import           Data.Monoid
+import           Data.Maybe                  (fromMaybe)
 import qualified Data.Text                as T
 import           Data.Text.Format
 import qualified Data.Text.IO             as TIO
@@ -442,9 +443,15 @@
     thyXTs     =                    filter (isKind 1) xts
     qryXTs     = Misc.mapSnd tx <$> filter (isKind 2) xts
     isKind n   = (n ==)  . symKind env . fst
-    xts        = F.toListSEnv           (F.seSort env)
+    xts        = symbolSorts (F.seSort env) -- F.toListSEnv           (F.seSort env)
     tx         = elaborate    "declare" env
     ats        = funcSortVars env
+
+symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
+symbolSorts env = [(x, tx t) | (x, t) <- F.toListSEnv env ]
+ where
+  tx t@(FObj a) = fromMaybe t (F.lookupSEnv a env)
+  tx t          = t
 
 dataDeclarations :: SymEnv -> [DataDecl]
 dataDeclarations = -- (if True then orderDeclarations else id) .
diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs
--- a/src/Language/Fixpoint/Smt/Serialize.hs
+++ b/src/Language/Fixpoint/Smt/Serialize.hs
@@ -139,6 +139,7 @@
   smt2 env (PAll   bs p)    = build "(forall ({}) {})"  (smt2s env bs, smt2 env p)
   smt2 env (PAtom r e1 e2)  = mkRel env r e1 e2
   smt2 env (ELam b e)       = smt2Lam env b e
+  smt2 env (ECoerc _ _ e)   = smt2 env e
   smt2 _   e                = panic ("smtlib2 Pred  " ++ show e)
 
 -- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors
diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
--- a/src/Language/Fixpoint/Smt/Theories.hs
+++ b/src/Language/Fixpoint/Smt/Theories.hs
@@ -13,6 +13,7 @@
 
        -- * Convert theory symbols
      , smt2Symbol
+
        -- * Preamble to initialize SMT
      , preamble
 
@@ -27,7 +28,7 @@
 
        -- * Theories
      , setEmpty, setEmp, setCap, setSub, setAdd, setMem
-     , setCom, setCup, setDif, setSng, mapSel, mapSto
+     , setCom, setCup, setDif, setSng, mapSel, mapCup, mapSto, mapDef
 
       -- * Query Theories
      , isSmt2App
@@ -49,16 +50,23 @@
 import qualified Data.Text
 import           Data.String                 (IsString(..))
 
---------------------------------------------------------------------------
--- | Set Theory ----------------------------------------------------------
---------------------------------------------------------------------------
 
+{- | [NOTE:Adding-Theories] To add new (SMTLIB supported) theories to
+     liquid-fixpoint and upstream, grep for "Map_default" and then add
+     your corresponding symbol in all those places.
+     This is currently far more complicated than it needs to be.
+ -}
+
+--------------------------------------------------------------------------------
+-- | Theory Symbols ------------------------------------------------------------
+--------------------------------------------------------------------------------
+
 elt, set, map :: Raw
 elt  = "Elt"
 set  = "Set"
 map  = "Map"
 
-emp, add, cup, cap, mem, dif, sub, com, sel, sto :: Raw
+emp, add, cup, cap, mem, dif, sub, com, sel, sto, mcup, mdef :: Raw
 emp   = "smt_set_emp"
 add   = "smt_set_add"
 cup   = "smt_set_cup"
@@ -69,8 +77,11 @@
 com   = "smt_set_com"
 sel   = "smt_map_sel"
 sto   = "smt_map_sto"
+mcup  = "smt_map_cup"
+mdef  = "smt_map_def"
 
-setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng, mapSel, mapSto :: Symbol
+
+setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: Symbol
 setEmpty = "Set_empty"
 setEmp   = "Set_emp"
 setCap   = "Set_cap"
@@ -81,9 +92,12 @@
 setCup   = "Set_cup"
 setDif   = "Set_dif"
 setSng   = "Set_sng"
+
+mapSel, mapSto, mapCup, mapDef :: Symbol
 mapSel   = "Map_select"
 mapSto   = "Map_store"
-
+mapCup   = "Map_union"
+mapDef   = "Map_default"
 
 strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol
 strLen    = "strLen"
@@ -132,6 +146,10 @@
         (sel, map, elt, elt)
     , format "(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"
         (sto, map, elt, elt, map)
+    , format "(define-fun {} ((m1 {}) (m2 {})) {} ((_ map (+ ({} {}) {})) m1 m2))"
+        (mcup, map, map, map, elt, elt, elt)
+    , format "(define-fun {} ((v {})) {} ((as const ({})) v))"
+        (mdef, elt, map, map)
     , format "(define-fun {} ((b Bool)) Int (ite b 1 0))"
         (Only (boolToIntName :: T.Text))
     , uifDef u (symbolText mulFuncName) ("*"   :: T.Text)
@@ -254,10 +272,6 @@
 
 smt2App _ _ _ _    = Nothing
 
--- smt2App env (EVar f) (d:ds)
---  | Just s <- {- tracepp ("SYMENVTHEORY: " ++ showpp f) $ -} symEnvTheory f env
---  = Just $ build "({} {})" (tsRaw s, d <> mconcat [ " " <> d | d <- ds])
-
 smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder.Builder
 smt2AppArg k env (ECst (EVar f) t)
   | Just fThy <- symEnvTheory f env
@@ -265,10 +279,6 @@
             then (k env f (ffuncOut t))
             else (build "{}" (Only (tsRaw fThy)))
 
--- // smt2AppArg _ env (EVar f)
--- // | Just fThy <- symEnvTheory f env
--- //  = Just (build "{}" (Only (tsRaw fThy)))
-
 smt2AppArg _ _ _
   = Nothing
 
@@ -308,8 +318,6 @@
 --   to avoid duplicate SMT definitions.  `uninterpSEnv` is for uninterpreted
 --   symbols, and `interpSEnv` is for interpreted symbols.
 --------------------------------------------------------------------------------
--- theorySEnv :: SEnv Sort
--- theorySEnv = fromListSEnv . M.toList . fmap tsSort $ theorySymbols
 
 -- | `theorySymbols` contains the list of ALL SMT symbols with interpretations,
 --   i.e. which are given via `define-fun` (as opposed to `declare-fun`)
@@ -333,6 +341,8 @@
   , interpSym setCom   com   setCmpSort
   , interpSym mapSel   sel   mapSelSort
   , interpSym mapSto   sto   mapStoSort
+  , interpSym mapCup   mcup  mapCupSort
+  , interpSym mapDef   mdef  mapDefSort
   , interpSym bvOrName "bvor"   bvBopSort
   , interpSym bvAndName "bvand" bvBopSort
   , interpSym strLen    strLen    strLenSort
@@ -345,62 +355,26 @@
     setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)
     setMemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort
     setCmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort
-    mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) $ FFunc (FVar 0) (FVar 1)
+    mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))
+                                 $ FFunc (FVar 0) (FVar 1)
+    mapCupSort = FAbs 0          $ FFunc (mapSort (FVar 0) intSort)
+                                 $ FFunc (mapSort (FVar 0) intSort)
+                                         (mapSort (FVar 0) intSort)
     mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))
                                  $ FFunc (FVar 0)
                                  $ FFunc (FVar 1)
                                          (mapSort (FVar 0) (FVar 1))
+    mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1)
+                                         (mapSort (FVar 0) (FVar 1))
+
     bvBopSort  = FFunc bitVecSort $ FFunc bitVecSort bitVecSort
 
 
 interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
 interpSym x n t = (x, Thy x n t Theory)
 
--- SHIFTLAM _uninterpSymbols :: [(Symbol, TheorySymbol)]
--- SHIFTLAM _uninterpSymbols = [ (x, uninterpSym x t) | (x, t) <- _uninterpSymbols']
--- SHIFTLAM
--- SHIFTLAM --------------------------------------------------------------------------------
--- SHIFTLAM _uninterpSym :: Symbol -> Sort -> TheorySymbol
--- SHIFTLAM --------------------------------------------------------------------------------
--- SHIFTLAM _uninterpSym x t =  Thy x (symbolRaw x) t Uninterp
--- SHIFTLAM
--- SHIFTLAM _uninterpSymbols' :: [(Symbol, Sort)]
--- SHIFTLAM _uninterpSymbols' = [] -- [ (toIntName,  mkFFunc 1 [FVar 0, FInt]) ]
-
-  -- SHIFTLAM  [ (setToIntName,    FFunc (setSort intSort)   intSort)
-  -- SHIFTLAM  , (bitVecToIntName, FFunc bitVecSort intSort)
-  -- SHIFTLAM  , (mapToIntName,    FFunc (mapSort intSort intSort) intSort)
-  -- SHIFTLAM  , (realToIntName,   FFunc realSort   intSort)
-  -- SHIFTLAM  , (lambdaName   ,   FFunc intSort (FFunc intSort intSort))
-  -- SHIFTLAM  ]
-  -- SHIFTLAM  ++ concatMap makeApplies [1..maxLamArg]
-  -- SHIFTLAM  ++ [(lamArgSymbol i, s) | i <- [1..maxLamArg], s <- sorts]
--- SHIFTLAM
--- SHIFTLAM  -- THESE ARE DUPLICATED IN DEFUNCTIONALIZATION
-
 maxLamArg :: Int
 maxLamArg = 7
-
--- SHIFTLAM sorts :: [Sort]
--- SHIFTLAM sorts = [intSort]
-
--- NIKI TODO: allow non integer lambda arguments
--- sorts = [setSort intSort, bitVecSort intSort, mapSort intSort intSort, boolSort, realSort, intSort]
--- makeLamArg :: Sort -> Int  -> Symbol
--- makeLamArg _ = intArgName
-
--- SHIFTLAM makeApplies :: Int -> [(Symbol, Sort)]
--- SHIFTLAM makeApplies i =
-  -- SHIFTLAM [ (intApplyName i,    go i intSort)
-  -- SHIFTLAM , (setApplyName i,    go i (setSort intSort))
-  -- SHIFTLAM , (bitVecApplyName i, go i bitVecSort)
-  -- SHIFTLAM , (mapApplyName i,    go i $ mapSort intSort intSort)
-  -- SHIFTLAM , (realApplyName i,   go i realSort)
-  -- SHIFTLAM , (boolApplyName i,   go i boolSort)
-  -- SHIFTLAM ]
-  -- SHIFTLAM where
-    -- SHIFTLAM go 0 s = FFunc intSort s
-    -- SHIFTLAM go i s = FFunc intSort $ go (i-1) s
 
 axiomLiterals :: [(Symbol, Sort)] -> [Expr]
 axiomLiterals lts = catMaybes [ lenAxiom l <$> litLen l | (l, t) <- lts, isString t ]
diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs
--- a/src/Language/Fixpoint/Solver.hs
+++ b/src/Language/Fixpoint/Solver.hs
@@ -16,15 +16,19 @@
 
     -- * Parse Qualifiers from File
   , parseFInfo
+
+    -- * Simplified Info
+  , simplifyFInfo
 ) where
 
 import           Control.Concurrent
 import           Data.Binary
 import           System.Exit                        (ExitCode (..))
-import           System.Console.CmdArgs.Verbosity   (whenNormal)
+import           System.Console.CmdArgs.Verbosity   (whenNormal, whenLoud)
 import           Text.PrettyPrint.HughesPJ          (render)
 import           Control.Monad                      (when)
 import           Control.Exception                  (catch)
+
 import           Language.Fixpoint.Solver.Sanitize  (symbolEnv, sanitize)
 import           Language.Fixpoint.Solver.UniqifyBinds (renameAll)
 import           Language.Fixpoint.Defunctionalize (defunctionalize)
@@ -174,7 +178,9 @@
   where
     msg           = "fq file after Uniqify & Rename " ++ show i ++ "\n"
 
-solveNative' !cfg !fi0 = do
+simplifyFInfo :: (NFData a, Fixpoint a, Show a, Loc a)
+               => Config -> FInfo a -> IO (SInfo a)
+simplifyFInfo !cfg !fi0 = do
   -- writeLoud $ "fq file in: \n" ++ render (toFixpoint cfg fi)
   -- rnf fi0 `seq` donePhase Loud "Read Constraints"
   -- let qs   = quals fi0
@@ -190,17 +196,19 @@
   graphStatistics cfg si1
   let si2  = {-# SCC "wfcUniqify" #-} wfcUniqify $!! si1
   let si3  = {-# SCC "renameAll"  #-} renameAll  $!! si2
-  rnf si3 `seq` donePhase Loud "Uniqify & Rename"
+  rnf si3 `seq` whenLoud $ donePhase Loud "Uniqify & Rename"
   loudDump 1 cfg si3
   let si4  = {-# SCC "defunction" #-} defunctionalize cfg $!! si3
+  -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)
   loudDump 2 cfg si4
-  rnf si4 `seq` donePhase Loud "Defunctionalize"
   let si5  = {-# SCC "elaborate"  #-} elaborate "solver" (symbolEnv cfg si4) si4
   loudDump 3 cfg si5
-  rnf si5 `seq` donePhase Loud "Elaborate"
-  si6 <- {-# SCC "Sol.inst"  #-} instantiate cfg $!! si5
-  rnf si6 `seq` donePhase Loud "Instantiate"
+  instantiate cfg $!! si5
+
+solveNative' !cfg !fi0 = do
+  si6 <- simplifyFInfo cfg fi0
   res <- {-# SCC "Sol.solve" #-} Sol.solve cfg $!! si6
+  -- rnf soln `seq` donePhase Loud "Solve2"
   --let stat = resStatus res
   saveSolution cfg res
   -- when (save cfg) $ saveSolution cfg
diff --git a/src/Language/Fixpoint/Solver/GradualSolution.hs b/src/Language/Fixpoint/Solver/GradualSolution.hs
--- a/src/Language/Fixpoint/Solver/GradualSolution.hs
+++ b/src/Language/Fixpoint/Solver/GradualSolution.hs
@@ -11,6 +11,7 @@
 import qualified Data.List                      as L
 import           Data.Maybe                     (maybeToList, isNothing)
 import           Data.Monoid                    ((<>))
+import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.Types.PrettyPrint ()
 import qualified Language.Fixpoint.SortCheck          as So
 import           Language.Fixpoint.Misc
@@ -18,20 +19,26 @@
 import qualified Language.Fixpoint.Types.Solutions    as Sol
 import           Language.Fixpoint.Types.Constraints  hiding (ws, bs)
 import           Prelude                              hiding (init, lookup)
-
+import           Language.Fixpoint.Solver.Sanitize  (symbolEnv)
+import Language.Fixpoint.SortCheck
 
 --------------------------------------------------------------------------------
 -- | Initial Gradual Solution (from Qualifiers and WF constraints) -------------
 --------------------------------------------------------------------------------
-init :: (F.Fixpoint a) => F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))]
+init :: (F.Fixpoint a) => Config -> F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))]
 --------------------------------------------------------------------------------
-init si = map (refineG si qs genv) gs `using` parList rdeepseq 
+init cfg si = map (elab . refineG si qs genv) gs `using` parList rdeepseq 
   where
     qs         = F.quals si
     gs         = snd <$> gs0
     genv       = instConstants si
 
     gs0        = L.filter (isGWfc . snd) $ M.toList (F.ws si)
+
+    elab (k,(x,es)) = ((k,) . (x,)) $ (elaborate "init" (sEnv (gsym x) (gsort x)) <$> es)
+    
+    sEnv x s    = isEnv {F.seSort = F.insertSEnv x s (F.seSort isEnv)}
+    isEnv       = symbolEnv cfg si
 
 
 --------------------------------------------------------------------------------
diff --git a/src/Language/Fixpoint/Solver/Instantiate.hs b/src/Language/Fixpoint/Solver/Instantiate.hs
--- a/src/Language/Fixpoint/Solver/Instantiate.hs
+++ b/src/Language/Fixpoint/Solver/Instantiate.hs
@@ -19,6 +19,7 @@
 import           Language.Fixpoint.Types.Config  as FC
 import qualified Language.Fixpoint.Types.Visitor as Vis
 import qualified Language.Fixpoint.Misc          as Misc -- (mapFst)
+import           Language.Fixpoint.Misc          ((<<=))
 import qualified Language.Fixpoint.Smt.Interface as SMT
 import           Language.Fixpoint.Defunctionalize
 import           Language.Fixpoint.SortCheck
@@ -31,15 +32,14 @@
 import qualified Data.Text            as T
 import qualified Data.HashMap.Strict  as M
 import qualified Data.List            as L
-import           Data.Maybe           (catMaybes, fromMaybe)
+import           Data.Maybe           (isNothing, catMaybes, fromMaybe)
 import           Data.Char            (isUpper)
--- import           Data.Foldable        (foldlM)
+-- import           Text.Printf (printf)
 
 (~>) :: (Expr, String) -> Expr -> EvalST Expr
 (_e,_str) ~> e' = do
-    modify (\st -> st{evId = evId st + 1})
-    -- traceM $ showpp _str ++ " : " ++ showpp _e ++ showpp e'
-    return (η e')
+    modify (\st -> st {evId = evId st + 1})
+    return (wtf e')
 
 
 --------------------------------------------------------------------------------
@@ -54,10 +54,11 @@
 instantiate' cfg fi = sInfo cfg fi env <$> withCtx cfg file env act
   where
     act ctx         = forM cstrs $ \(i, c) ->
-                        (i,) . notracepp ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs fi) (ae fi) i c
+                        (i,) . notracepp ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs fi) aenv i c
     cstrs           = M.toList (cm fi)
     file            = srcFile cfg ++ ".evals"
     env             = symbolEnv cfg fi
+    aenv            = {- tracepp "AXIOM-ENV" -} (ae fi)
 
 sInfo :: Config -> GInfo SimpC a -> SymEnv -> [(SubcId, Expr)] -> SInfo a
 sInfo cfg fi env ips = strengthenHyp fi' (notracepp "ELAB-INST:  " $ zip is ps'')
@@ -115,12 +116,8 @@
 --------------------------------------------------------------------------------
 -- | Knowledge (SMT Interaction)
 --------------------------------------------------------------------------------
--- AT:@TODO: knSels and knEqs should really just be the same thing. In this way,
--- we should also unify knSims and knAms, as well as their analogues in AxiomEnv
 data Knowledge
-  = KN { knSels    :: ![(Expr, Expr)]
-       , knEqs     :: ![(Expr, Expr)]
-       , knSims    :: ![Rewrite]
+  = KN { knSims    :: ![Rewrite]
        , knAms     :: ![Equation]
        , knContext :: IO SMT.Context
        , knPreds   :: !([(Symbol, Sort)] -> Expr -> SMT.Context -> IO Bool)
@@ -128,17 +125,7 @@
        }
 
 emptyKnowledge :: IO SMT.Context -> Knowledge
-emptyKnowledge ctx = KN [] [] [] [] ctx (\_ _ _ -> return False) []
-
-lookupKnowledge :: Knowledge -> Expr -> Maybe Expr
-lookupKnowledge γ e
-  -- Zero argument axioms like `mempty = N`
-  | Just e' <- L.lookup e (knEqs γ)
-  = Just e'
-  | Just e' <- L.lookup e (knSels γ)
-  = Just e'
-  | otherwise
-  = Nothing
+emptyKnowledge ctx = KN [] [] ctx (\_ _ _ -> return False) []
 
 isValid :: Knowledge -> Expr -> IO Bool
 isValid γ b = knPreds γ (knLams γ) b =<< knContext γ
@@ -147,9 +134,7 @@
                  -> [(Symbol, SortedReft)]
                  -> ([(Expr, Expr)], Knowledge)
 makeKnowledge cfg ctx aenv es = (simpleEqs,) $ (emptyKnowledge context)
-                                     { knSels   = sels
-                                     , knEqs    = eqs
-                                     , knSims   = aenvSimpl aenv
+                                     { knSims   = aenvSimpl aenv
                                      , knAms    = aenvEqs aenv
                                      , knPreds  = \bs e c -> askSMT c bs e
                                      }
@@ -165,28 +150,13 @@
                               ))
       return ctx
 
-    -- This creates the rewrite rule e1 -> e2
-    -- when should I apply it?
+    -- This creates the rewrite rule e1 -> e2. When should I apply it?
     -- 1. when e2 is a data con and can lead to further reductions
     -- 2. when size e2 < size e1
-    -- @TODO: Can this be generalized?
-    -- simpleEqs = []
-    simpleEqs = {- tracepp "SIMPLEEQS" $ -} _makeSimplifications (aenvSimpl aenv) =<<
-               L.nub (catMaybes [_getDCEquality e1 e2 | PAtom Eq e1 e2 <- atms])
+    simpleEqs = {- tracepp "SIMPLEEQS" $ -} makeSimplifications (aenvSimpl aenv) =<<
+               L.nub (catMaybes [_getDCEquality senv e1 e2 | PAtom Eq e1 e2 <- atms])
     atms = splitPAnd =<< (expr <$> filter isProof es)
     isProof (_, RR s _) = showpp s == "Tuple"
-    sels = (go . expr) =<< es
-    go e = let es   = splitPAnd e
-               su   = mkSubst [(x, EVar y)  | PAtom Eq (EVar x) (EVar y) <- es ]
-               sels = [(EApp (EVar s) x, e) | PAtom Eq (EApp (EVar s) x) e <- es
-                                            , isSelector s ]
-           in L.nub (sels ++ subst su sels)
-
-    eqs = [(EVar x, ex) | Equ a _ bd <- filter (null . eqArgs) $ aenvEqs aenv
-                        , PAtom Eq (EVar x) ex <- splitPAnd bd
-                        , x == a
-                        ]
-
     toSMT bs = defuncAny cfg senv . elaborate "makeKnowledge" (elabEnv bs)
     elabEnv  = L.foldl' (\env (x, s) -> insertSymEnv x s env) senv
 
@@ -195,7 +165,7 @@
     askSMT :: SMT.Context -> [(Symbol, Sort)] -> Expr -> IO Bool
     askSMT ctx bs e
       | isTautoPred  e = return True
-      | isContraPred e = return False
+    -- // Why?  | isContraPred e = return False -- Why the f?
       | null (Vis.kvars e) = do
           SMT.smtPush ctx
           b <- SMT.checkValid' ctx [] PTrue (toSMT bs e)
@@ -203,13 +173,9 @@
           return b
       | otherwise      = return False
 
-    -- TODO: Stringy hacks
-    isSelector :: Symbol -> Bool
-    isSelector  = L.isPrefixOf "select" . symbolString
-
-_makeSimplifications :: [Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)]
-_makeSimplifications sis (dc, es, e)
- = go =<< sis
+makeSimplifications :: [Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)]
+makeSimplifications sis (dc, es, e)
+     = go =<< sis
  where
    go (SMeasure f dc' xs bd)
      | dc == dc', length xs == length es
@@ -217,8 +183,8 @@
    go _
      = []
 
-_getDCEquality :: Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
-_getDCEquality e1 e2
+_getDCEquality :: SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
+_getDCEquality senv e1 e2
     | Just dc1 <- f1
     , Just dc2 <- f2
     = if dc1 == dc2
@@ -231,19 +197,23 @@
     | otherwise
     = Nothing
   where
-    (f1, es1) = Misc.mapFst getDC $ splitEApp e1
-    (f2, es2) = Misc.mapFst getDC $ splitEApp e2
+    (f1, es1) = Misc.mapFst (getDC senv) (splitEApp e1)
+    (f2, es2) = Misc.mapFst (getDC senv) (splitEApp e2)
 
-    -- TODO: Stringy hacks
-    getDC (EVar x)
-      = if isUpper $ head $ symbolString $ dropModuleNames x
-          then Just x
-          else Nothing
-    getDC _
-      = Nothing
+-- TODO: Stringy hacks
+getDC :: SymEnv -> Expr -> Maybe Symbol
+getDC senv (EVar x)
+  | isUpperSymbol x && isNothing (symEnvTheory x senv)
+  = Just x
+getDC _ _
+  = Nothing
 
-    dropModuleNames = mungeNames (symbol . last) "."
+isUpperSymbol :: Symbol -> Bool
+isUpperSymbol = isUpper . headSym . dropModuleNames
 
+dropModuleNames :: Symbol -> Symbol
+dropModuleNames = mungeNames (symbol . last) "."
+  where
     mungeNames _ _ ""  = ""
     mungeNames f d s'@(symbolText -> s)
       | s' == tupConName = tupConName
@@ -260,20 +230,58 @@
 --------------------------------------------------------------------------------
 -- AT@TODO do this for all reflected functions, not just DataCons
 
--- Insert measure info for every constructor
--- that appears in the expression e
--- required by PMEquivalence.mconcatChunk
--- ADTs does this automatically
+{- [NOTE:Datacon-Selectors] The 'assertSelectors' function
+   insert measure information for every constructor that appears
+   in the expression e.
+
+   In theory, this is not required as the SMT ADT encoding takes
+   care of it. However, in practice, some constructors, e.g. from
+   GADTs cannot be directly encoded in SMT due to the lack of SMTLIB
+   support for GADT. Hence, we still need to hang onto this code.
+
+   See tests/proof/ple2.fq for a concrete example.
+ -}
+
 assertSelectors :: Knowledge -> Expr -> EvalST ()
-assertSelectors _ _ = return ()
+-- assertSelectors _ _ = return ()
+{- TODO: HEREHEREHEREHEREHEREHERE
+  1. DOES this kill Unification.hs? (Guard under --no-adt)
+  2. Use addEquality instead off _addSMTEquality.
+-}
+assertSelectors γ e = do
+    sims <- aenvSimpl <$> gets _evAEnv
+    -- cfg  <- gets evCfg
+    -- _    <- foldlM (\_ s -> Vis.mapMExpr (go s) e) (tracepp "assertSelector" e) sims
+    forM_ sims $ \s -> Vis.mapMExpr (go s) e
+    return ()
+  where
+    go :: Rewrite -> Expr -> EvalST Expr
+    go (SMeasure f dc xs bd) e@(EApp _ _)
+      | (EVar dc', es) <- splitEApp e
+      , dc == dc'
+      , length xs == length es
+      = do let e1 = (EApp (EVar f) e)
+           let e2 = (subst (mkSubst $ zip xs es) bd)
+           addEquality γ e1 e2
+           return e
+    go _ e
+      = return e
 
+-- _addSMTEquality :: Knowledge -> Expr -> Expr -> IO ()
+-- _addSMTEquality γ e1 e2 = do
+  -- ctx <- knContext γ
+  -- SMT.smtAssert ctx (tracepp "addSMTEQ" (PAtom Eq (makeLam γ e1) (makeLam γ e2)))
+
 --------------------------------------------------------------------------------
 -- | Symbolic Evaluation with SMT
 --------------------------------------------------------------------------------
-data EvalEnv = EvalEnv { evId        :: Int
-                       , evSequence  :: [(Expr,Expr)]
-                       , _evAEnv     :: AxiomEnv
-                       }
+data EvalEnv = EvalEnv
+  { evId        :: !Int
+  , evSequence  :: [(Expr,Expr)]
+  , _evAEnv     :: !AxiomEnv
+  , evEnv       :: !SymEnv
+  , _evCfg      :: !Config
+  }
 
 type EvalST a = StateT EvalEnv IO a
 
@@ -285,13 +293,14 @@
     (fmap join . sequence)
     (evalOne <$> L.nub (grepTopApps =<< einit))
   where
-    (eqs, γ) = makeKnowledge cfg ctx aenv facts
-    initEvalSt = EvalEnv 0 [] aenv
+    (eqs, γ)   = makeKnowledge cfg ctx aenv facts
+    senv       = SMT.ctxSymEnv ctx
+    initEvalSt = EvalEnv 0 [] aenv senv cfg
     -- This adds all intermediate unfoldings into the assumptions
     -- no test needs it
     -- TODO: add a flag to enable it
     evalOne :: Expr -> IO [(Expr, Expr)]
-    evalOne e = do
+    evalOne e = {- notracepp ("evalOne e = " ++ showpp e) <$> -} do
       (e', st) <- runStateT (eval γ e) initEvalSt
       if e' == e then return [] else return ((e, e'):evSequence st)
 
@@ -308,27 +317,24 @@
 grepTopApps e@(EApp _ _)    = [e]
 grepTopApps _               = []
 
--- AT: I think makeLam is the adjoint of splitEApp?
+-- makeLam is the adjoint of splitEApp
 makeLam :: Knowledge -> Expr -> Expr
-makeLam γ e = foldl (flip ELam) e (knLams γ)
+makeLam γ e = L.foldl' (flip ELam) e (knLams γ)
 
 eval :: Knowledge -> Expr -> EvalST Expr
-eval γ e | Just e' <- lookupKnowledge γ e
-  = (e, "Knowledge") ~> e'
 eval γ (ELam (x,s) e)
-  -- SHIFTLAM (assuming this shifting is redundant if DEFUNC has already happened)
-  -- = do let x' = lamArgSymbol (1 + length (knLams γ))
-       -- e'    <- eval γ{knLams = (x',s):knLams γ} (subst1 e (x, EVar x'))
-       -- return $ ELam (x,s) $ subst1 e' (x', EVar x)
-
   = do e'    <- eval γ{knLams = (x, s) : knLams γ} e
        return $ ELam (x, s) e'
 
 eval γ e@(EIte b e1 e2)
   = do b' <- eval γ b
        evalIte γ e b' e1 e2
+eval γ (ECoerc s t e)
+  = ECoerc s t <$> eval γ e
 eval γ e@(EApp _ _)
   = evalArgs γ e >>= evalApp γ e
+eval γ e@(EVar _)
+  = evalApp γ e (e,[])
 eval γ (PAtom r e1 e2)
   = PAtom r <$> eval γ e1 <*> eval γ e2
 eval γ (ENeg e)
@@ -368,53 +374,136 @@
 evalApp :: Knowledge -> Expr -> (Expr, [Expr]) -> EvalST Expr
 evalApp γ e (EVar f, [ex])
   | (EVar dc, es) <- splitEApp ex
-  , Just simp <- L.find (\simp -> (smName simp == f) && (smDC simp == dc))
-                        (knSims γ)
+  , Just simp <- L.find (\simp -> (smName simp == f) && (smDC simp == dc)) (knSims γ)
   , length (smArgs simp) == length es
-  = do e'    <- eval γ $ η $ substPopIf (zip (smArgs simp) es) (smBody simp)
+  = do e'    <- eval γ $ wtf $ substPopIf (zip (smArgs simp) es) (smBody simp)
        (e, "Rewrite -" ++ showpp f) ~> e'
 evalApp γ _ (EVar f, es)
+  -- we should move the lookupKnowledge stuff here into kmAms γ
   | Just eq <- L.find ((==f) . eqName) (knAms γ)
   , Just bd <- getEqBody eq
   , length (eqArgs eq) == length es
-  , f `notElem` syms bd -- not recursive
-  = eval γ $ η $ substPopIf (zip (eqArgs eq) es) bd
+  , f `notElem` syms bd               -- non-recursive equations
+  = eval γ . wtf =<< assertSelectors γ <<= substEq PopIf eq es bd
+
 evalApp γ _e (EVar f, es)
   | Just eq <- L.find ((==f) . eqName) (knAms γ)
   , Just bd <- getEqBody eq
-  , length (eqArgs eq) == length es  --  recursive
-  = evalRecApplication γ (eApps (EVar f) es) $
-    subst (mkSubst $ zip (eqArgs eq) es) bd
+  , length (eqArgs eq) == length es   -- recursive equations
+  = evalRecApplication γ (eApps (EVar f) es) =<< substEq Normal eq es bd
 evalApp _ _ (f, es)
   = return $ eApps f es
 
+--------------------------------------------------------------------------------
+-- | 'substEq' unfolds or instantiates an equation at a particular list of
+--   argument values. We must also substitute the sort-variables that appear
+--   as coercions. See tests/proof/ple1.fq
+--------------------------------------------------------------------------------
+substEq :: SubstOp -> Equation -> [Expr] -> Expr -> EvalST Expr
+substEq o eq es bd = substEqVal o eq es <$> substEqCoerce eq es bd
+
+data SubstOp = PopIf | Normal
+
+substEqVal :: SubstOp -> Equation -> [Expr] -> Expr -> Expr
+substEqVal o eq es bd = case o of
+    PopIf  -> substPopIf     xes  bd
+    Normal -> subst (mkSubst xes) bd
+  where
+    xes    =  zip xs es
+    xs     =  eqArgNames eq
+
+substEqCoerce :: Equation -> [Expr] -> Expr -> EvalST Expr
+substEqCoerce eq es bd = do
+  env      <- seSort <$> gets evEnv
+  let ts    = snd    <$> eqArgs eq
+  let coSub = mkCoSub env es ts
+  return    $ applyCoSub coSub bd
+
+-- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'
+--   to the ty-vars that they should be substituted with. Note the
+--   domain and range are both Symbol and not the Int used for real ty-vars.
+
+type CoSub = M.HashMap Symbol Symbol
+
+mkCoSub :: SEnv Sort -> [Expr] -> [Sort] -> CoSub
+mkCoSub env es xTs = Misc.safeFromList "mkCoSub" xys
+  where
+    eTs            = sortExpr sp env <$> es
+    sp             = panicSpan "mkCoSub"
+    xys            = concat (zipWith matchSorts xTs eTs)
+
+matchSorts :: Sort -> Sort -> [(Symbol, Symbol)]
+matchSorts = go
+  where
+    go (FObj x)      (FObj y)      = [(x, y)]
+    go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2
+    go (FFunc s1 t1) (FFunc s2 t2) = go s1 s2 ++ go t1 t2
+    go (FApp s1 t1)  (FApp s2 t2)  = go s1 s2 ++ go t1 t2
+    go _             _             = []
+
+applyCoSub :: CoSub -> Expr -> Expr
+applyCoSub coSub      = Vis.mapExpr fE
+  where
+    fE (ECoerc s t e) = ECoerc (txS s) (txS t) e
+    fE e              = e
+    txS               = Vis.mapSort fS
+    fS (FObj a)       = FObj   (txV a)
+    fS t              = t
+    txV a             = M.lookupDefault a a coSub
+
+--------------------------------------------------------------------------------
+getEqBody :: Equation -> Maybe Expr
+getEqBody (Equ x xts b _ _)
+  | Just (fxs, e) <- getEqBodyPred b
+  , (EVar f, es)  <- splitEApp fxs
+  , f == x
+  , es == (EVar . fst <$> xts)
+  = Just e
+getEqBody _
+  = Nothing
+
+getEqBodyPred :: Expr -> Maybe (Expr, Expr)
+getEqBodyPred (PAtom Eq fxs e)
+  = Just (fxs, e)
+getEqBodyPred (PAnd ((PAtom Eq fxs e):_))
+  = Just (fxs, e)
+getEqBodyPred _
+  = Nothing
+
+eqArgNames :: Equation -> [Symbol]
+eqArgNames = map fst . eqArgs
+
 substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
-substPopIf xes e = η $ foldl go e xes
+substPopIf xes e = wtf $ L.foldl' go e xes
   where
     go e (x, EIte b e1 e2) = EIte b (subst1 e (x, e1)) (subst1 e (x, e2))
     go e (x, ex)           = subst1 e (x, ex)
 
 evalRecApplication :: Knowledge -> Expr -> Expr -> EvalST Expr
-evalRecApplication γ e (EIte b e1 e2)
-  = do b' <- eval γ b
-       b'' <- liftIO (isValid γ b')
-       if b''
-          then addApplicationEq γ e e1 >>
-               ({-# SCC "assertSelectors-1" #-} assertSelectors γ e1) >>
-               eval γ e1 >>=
-               ((e, "App") ~>)
-          else do b''' <- liftIO (isValid γ (PNot b'))
-                  if b'''
-                     then addApplicationEq γ e e2 >>
-                          ({-# SCC "assertSelectors-1" #-} assertSelectors γ e2) >>
-                          eval γ e2 >>=
-                          ((e, "App") ~>)
-                     else return e
+evalRecApplication γ e (EIte b e1 e2) = do
+  contra <- {- tracepp ("CONTRA? " ++ showpp e) <$> -} liftIO (isValid γ PFalse)
+  if contra
+    then return e
+    else do b' <- eval γ b
+            b1 <- liftIO (isValid γ b')
+            if b1
+              then addEquality γ e e1 >>
+                   ({-# SCC "assertSelectors-1" #-} assertSelectors γ e1) >>
+                   eval γ e1 >>=
+                   ((e, "App") ~>)
+              else do
+                   b2 <- liftIO (isValid γ (PNot b'))
+                   if b2
+                      then addEquality γ e e2 >>
+                           ({-# SCC "assertSelectors-2" #-} assertSelectors γ e2) >>
+                           eval γ e2 >>=
+                           ((e, "App") ~>)
+                      else return e
 evalRecApplication _ _ e
   = return e
 
-addApplicationEq :: Knowledge -> Expr -> Expr -> EvalST ()
-addApplicationEq γ e1 e2 =
+addEquality :: Knowledge -> Expr -> Expr -> EvalST ()
+addEquality γ e1 e2 =
   modify (\st -> st{evSequence = (makeLam γ e1, makeLam γ e2):evSequence st})
 
 evalIte :: Knowledge -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
@@ -438,10 +527,14 @@
        e2' <- eval γ e2
        return $ EIte b e1' e2'
 
+--------------------------------------------------------------------------------
 -- normalization required by ApplicativeMaybe.composition
----------------------------------------------------------
-η :: Expr -> Expr
-η = snd . go
+--------------------------------------------------------------------------------
+-- RJ: What on earth is this function doing?
+wtf :: Expr -> Expr
+wtf = id
+{-
+wtf = snd . go
   where
     go (EIte b t f)
       | isTautoPred t && isFalse f
@@ -465,5 +558,6 @@
               else (False, EApp e1' e2')
     go e = (False, e)
 
+-}
 instance Expression (Symbol, SortedReft) where
   expr (x, RR _ (Reft (v, r))) = subst1 (expr r) (v, EVar x)
diff --git a/src/Language/Fixpoint/Solver/Solve.hs b/src/Language/Fixpoint/Solver/Solve.hs
--- a/src/Language/Fixpoint/Solver/Solve.hs
+++ b/src/Language/Fixpoint/Solver/Solve.hs
@@ -8,7 +8,7 @@
 -- | Solve a system of horn-clause constraints ---------------------------------
 --------------------------------------------------------------------------------
 
-module Language.Fixpoint.Solver.Solve (solve) where
+module Language.Fixpoint.Solver.Solve (solve, solverInfo) where
 
 import           Control.Monad (when, filterM)
 import           Control.Monad.State.Strict (lift)
@@ -16,8 +16,6 @@
 import qualified Language.Fixpoint.Misc            as Misc
 import qualified Language.Fixpoint.Types           as F
 import qualified Language.Fixpoint.Types.Solutions as Sol
-import qualified Language.Fixpoint.Types.Graduals  as G
-import qualified Language.Fixpoint.Solver.GradualSolution as GS
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Config hiding (stats)
 import qualified Language.Fixpoint.Solver.Solution  as S
@@ -33,22 +31,15 @@
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet        as S
 import qualified Data.List as L
-import Control.Concurrent.ParallelIO.Global (parallel)
 
-import qualified Language.Fixpoint.SortCheck       as So
-import Language.Fixpoint.Solver.Sanitize (symbolEnv)
--- DEBUG
--- import           Debug.Trace (trace)
-
 --------------------------------------------------------------------------------
 solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> IO (F.Result (Integer, a))
 --------------------------------------------------------------------------------
-solve cfg fi | gradual cfg
- = solveGradual cfg fi
 
 solve cfg fi = do
-    donePhase Misc.Loud "Worklist Initialize"
-    (res, stat) <- withProgressFI sI $ runSolverM cfg sI act
+    whenLoud $ donePhase Misc.Loud "Worklist Initialize"
+    vb <- getVerbosity
+    (res, stat) <- (if (Quiet == vb || gradual cfg) then id else withProgressFI sI) $ runSolverM cfg sI act
     when (solverStats cfg) $ printStats fi wkl stat
     -- print (numIter stat)
     return res
@@ -61,124 +52,10 @@
 
 
 --------------------------------------------------------------------------------
-solveGradual :: (NFData a, F.Fixpoint a, Show a, F.Loc a)
-             => Config -> F.SInfo a -> IO (F.Result (Integer, a))
---------------------------------------------------------------------------------
-solveGradual cfg fi = do
-  -- graphStatistics cfg $ G.uniquify fi
-  let fis = zip [1..] $ partition' Nothing $ G.uniquify fi
-  if ginteractive cfg
-    then snd . traceShow "FINAL SOLUTION\n"  <$> iSolveGradual cfg fis
-    else snd . traceShow "FINAL SOLUTION\n" . mconcat <$> parallel (solveGradualOne cfg <$> fis)
-
-
-iSolveGradual :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> [(Int, F.SInfo a)] -> IO (Maybe G.GSol, F.Result (Integer, a))
-iSolveGradual cfg fis
-  = mconcat <$> parallel (solveGradualOne cfg <$> fis)
-
-
-solveGradualOne :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> (Int, F.SInfo a) -> IO (Maybe G.GSol, F.Result (Integer, a))
-solveGradualOne cfg (_, fi) = do
-  sols   <- makeSolutions cfg fi
-  gradualLoop (cfg{gradual = False}) fi sols
-
-gradualLoop :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> (Maybe [G.GSol]) -> IO (Maybe G.GSol, F.Result (Integer, a))
-gradualLoop _ _ Nothing
-  = return (Nothing, F.safe)
-gradualLoop _ _ (Just [])
-  = return (Nothing, F.unsafe)
-gradualLoop cfg fi (Just (s:ss))
-  = do whenLoud   $ putStrLn ("Solving for " ++ show s)
-       whenNormal $ putStr "*"
-       v <- getVerbosity
-       -- putStr ("Substitution = " ++ show s)
-       -- putStr ("BEFORE \n\n"  ++ (show $ F.toFixpoint cfg fi))
-       -- putStr ("AFTER \n\n"  ++ (show $ F.toFixpoint cfg $ G.gsubst s fi))
-       whenNormal $ setVerbosity Quiet
-       r <- solve cfg (G.gsubst s fi)
-       setVerbosity v
-       whenLoud $ putStrLn ("Solution = " ++ if F.isUnsafe r then "UNSAFE" else "SAFE")
-       if F.isUnsafe r
-        then gradualLoop cfg fi (Just ss)
-        else return (Just s, r)
-
-
-makeSolutions :: (NFData a, F.Fixpoint a, Show a) => Config -> F.SInfo a -> IO (Maybe [G.GSol])
-makeSolutions cfg fi
-  = G.makeSolutions cfg fi <$> makeLocalLattice cfg fi (GS.init fi)
-
-
-
-makeLocalLattice :: Config -> F.SInfo a
-                 -> [(F.KVar, (F.GWInfo, [F.Expr]))]
-                 -> IO [(F.KVar, (F.GWInfo, [[F.Expr]]))]
-makeLocalLattice cfg fi kes = runSolverM cfg sI (act kes)
-  where
-    sI  = solverInfo cfg fi
-    act = mapM (makeLocalLatticeOne cfg fi)
-
-
-makeLocalLatticeOne :: Config -> F.SInfo a
-            -> (F.KVar, (F.GWInfo, [F.Expr]))
-            -> SolveM (F.KVar, (F.GWInfo, [[F.Expr]]))
-makeLocalLatticeOne cfg fi (k, (e, es)) = do
-   elems0  <- filterM (isLocal e) (map (:[]) es)
-   elems   <- sortEquals elems0
-   lattice <- makeLattice [] (map (:[]) elems) elems
-   return $ ((k,) . (e,)) lattice
-  where
-    sEnv = symbolEnv cfg fi
-    makeLattice acc new elems
-      | null new
-      = return {- traceShow ("LATTICE FROM ELEMENTS = " ++ showElems elems  ++ showElemss acc) -} acc
-      | otherwise
-      = do let cands = [e:es | e <- elems, es <- new]
-           localCans <- filterM (isLocal e) cands
-           newElems  <- filterM (notTrivial (new ++ acc)) localCans
-           makeLattice (acc ++ new) newElems elems
-    _showElem :: F.Expr -> String
-    _showElem e1 = showpp $ F.subst (F.mkSubst [(x, F.EVar $ F.tidySymbol x) | x <- F.syms e1]) e1
-    _showElems = unlines . map _showElem
-    _showElemss = unlines. map _showElems
-
-    notTrivial [] _     = return True
-    notTrivial (x:xs) p = do v <- isValid F.dummySpan (mkPred x) (mkPred p)
-                             if v then return False
-                                  else notTrivial xs p
-
-    mkPred es = So.elaborate "initBGind.mkPred" sEnv (F.pAnd es)
-
-    isLocal i es = do
-      let pp = So.elaborate "filterLocal" sEnv $ F.PExist [(F.gsym i, F.gsort i)] $ F.pAnd (F.gexpr i:es)
-      isValid F.dummySpan mempty pp
-
-    root      = mempty
-    sortEquals xs = (bfs [0]) <$> makeEdges vs [] vs
-      where
-       vs        = zip [0..] (root:(head <$> xs))
-
-       bfs []     _  = []
-       bfs (i:is) es = (snd $ (vs!!i)) : bfs (is++map snd (filter (\(j,k) ->  (j==i && notElem k is)) es)) es
-
-       makeEdges _   acc []    = return acc
-       makeEdges vs acc (x:xs) = do ves  <- concat <$> mapM (makeEdgesOne x) vs
-                                    if any (\(i,j) -> elem (j,i) acc) ves
-                                      then makeEdges (filter ((/= fst x) . fst) vs) (filter (\(i,j) -> ((i /= fst x) && (j /= fst x))) acc) xs
-                                      else makeEdges vs (mergeEdges (ves ++ acc)) xs
-
-    makeEdgesOne (i,_) (j,_) | i == j = return []
-    makeEdgesOne (i,x) (j,y) = do
-      ij <- isValid F.dummySpan (mkPred [x]) (mkPred [y])
-      return (if ij then [(j,i)] else [])
-
-    mergeEdges es = filter (\(i,j) -> (not (any (\k -> ((i,k) `elem` es && (k,j) `elem` es)) (fst <$> es)))) es
-
---------------------------------------------------------------------------------
-
 -- | Progress Bar
 --------------------------------------------------------------------------------
 withProgressFI :: SolverInfo a b -> IO b -> IO b
-withProgressFI = withProgress . fromIntegral . cNumScc . siDeps
+withProgressFI = withProgress . (+ 1) . fromIntegral . cNumScc . siDeps  
 --------------------------------------------------------------------------------
 
 printStats :: F.SInfo a ->  W.Worklist a -> Stats -> IO ()
diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs
--- a/src/Language/Fixpoint/SortCheck.hs
+++ b/src/Language/Fixpoint/SortCheck.hs
@@ -28,6 +28,7 @@
   , sortExpr
   , checkSortExpr
   , exprSort
+  , exprSort_maybe
 
   -- * Unify
   , unifyFast
@@ -58,7 +59,7 @@
 
 import qualified Data.HashMap.Strict       as M
 import qualified Data.List                 as L
-import           Data.Maybe                (mapMaybe, fromMaybe)
+import           Data.Maybe                (mapMaybe, fromMaybe, catMaybes)
 
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Misc
@@ -198,13 +199,14 @@
     step (PAll   bs p)    = PAll   bs (go p)
     step (PAtom r e1 e2)  = PAtom r (go e1) (go e2)
     step e@(EApp {})      = go e
-    step (ELam b e)       = ELam b (go e)
+    step (ELam b e)       = ELam b       (go e)
+    step (ECoerc a t e)   = ECoerc a t   (go e)
     step (PGrad k su i e) = PGrad k su i (go e)
     step e@(PKVar {})     = e
     step e@(ESym {})      = e
     step e@(ECon {})      = e
     step e@(EVar {})      = e
-    -- ELam, ETApp, ETAbs, PAll, PExist
+    -- ETApp, ETAbs, PAll, PExist
     step e                = error $ "TODO elabApply: " ++ showpp e
 
 --------------------------------------------------------------------------------
@@ -357,6 +359,7 @@
 checkExpr f (PAll  bs e )  = checkExpr (addEnv f bs) e
 checkExpr f (PExist bs e)  = checkExpr (addEnv f bs) e
 checkExpr f (ELam (x,t) e) = FFunc t <$> checkExpr (addEnv f [(x,t)]) e
+checkExpr f (ECoerc s t e) = checkExpr f (ECst e s) >> return t 
 checkExpr _ (ETApp _ _)    = error "SortCheck.checkExpr: TODO: implement ETApp"
 checkExpr _ (ETAbs _ _)    = error "SortCheck.checkExpr: TODO: implement ETAbs"
 
@@ -379,11 +382,15 @@
 
 elab f (EApp e1@(EApp _ _) e2) = do
   (e1', _, e2', s2, s) <- notracepp "ELAB-EAPP" <$> elabEApp f e1 e2
-  return (eAppC s e1'          (ECst e2' s2), s)
+  let e = eAppC s e1' (ECst e2' s2)
+  let θ = unifyExpr (snd f) e
+  return (applyExpr θ e, maybe s (`apply` s) θ)
 
 elab f (EApp e1 e2) = do
   (e1', s1, e2', s2, s) <- elabEApp f e1 e2
-  return (eAppC s (ECst e1' s1) (ECst e2' s2), s)
+  let e = eAppC s (ECst e1' s1) (ECst e2' s2)
+  let θ = unifyExpr (snd f) e
+  return (applyExpr θ e, maybe s (`apply` s) θ)
 
 elab _ e@(ESym _) =
   return (e, strSort)
@@ -477,6 +484,10 @@
   let t' = elaborate "ELam Arg" mempty t
   return (ELam (x, t') (ECst e' s), FFunc t s)
 
+elab f (ECoerc s t e) = do
+  (e', _) <- elab f e
+  return     (ECoerc s t e', t)
+
 elab _ (ETApp _ _) =
   error "SortCheck.elab: TODO: implement ETApp"
 elab _ (ETAbs _ _) =
@@ -629,14 +640,24 @@
 -- | Expressions sort  ---------------------------------------------------------
 --------------------------------------------------------------------------------
 exprSort :: String -> Expr -> Sort
-exprSort msg = go
+exprSort msg e = fromMaybe (panic err) (exprSort_maybe e)
   where
-    go (ECst _ s) = s
-    go (ELam (_, sx) e) = FFunc sx (go e)
+    err        = printf "exprSort [%s] on unexpected expression %s" msg (show e)
+
+  -- case exprSort_maybe e of
+  --  Nothing -> errorstar ("\nexprSort [" ++ msg ++ "] on unexpected expressions " ++ show e)
+  --  Just s  -> s
+
+
+exprSort_maybe :: Expr -> Maybe Sort
+exprSort_maybe = go
+  where
+    go (ECst _ s) = Just s
+    go (ELam (_, sx) e) = FFunc sx <$> go e
     go (EApp e ex)
-      | FFunc sx s <- genSort (go e)
-      = maybe s (`apply` s) $ unifySorts (go ex) sx
-    go e = errorstar ("\nexprSort [" ++ msg ++ "] on unexpected expressions " ++ show e)
+      | Just (FFunc sx s) <- genSort <$> go e
+      = maybe s (`apply` s) <$> ((`unifySorts` sx) <$> go ex)
+    go _ = Nothing
 
 genSort :: Sort -> Sort
 genSort (FAbs _ t) = genSort t
@@ -650,10 +671,9 @@
 
 -- | Helper for checking symbol occurrences
 checkSym :: Env -> Symbol -> CheckM Sort
-checkSym f x
-  = case f x of
-     Found s -> instantiate s
-     Alts xs -> throwError $ errUnboundAlts x xs
+checkSym f x = case f x of
+  Found s -> instantiate s
+  Alts xs -> throwError (errUnboundAlts x xs)
 
 -- | Helper for checking if-then-else expressions
 checkIte :: Env -> Expr -> Expr -> Expr -> CheckM Sort
@@ -754,10 +774,20 @@
 checkNumeric :: Env -> Sort -> CheckM ()
 checkNumeric f s@(FObj l)
   = do t <- checkSym f l
-       unless (t == FNum || t == FFrac) (throwError $ errNonNumeric s)
+       unless (t `elem` [FNum, FFrac, intSort, FInt]) (throwError $ errNonNumeric s)
 checkNumeric _ s
   = unless (isNumeric s) (throwError $ errNonNumeric s)
 
+checkEqConstr :: Env -> Maybe Expr -> a -> Symbol -> Sort -> CheckM a
+checkEqConstr _ _  θ a (FObj b)
+  | a == b
+  = return θ
+checkEqConstr f e θ a t = do
+  case f a of
+    Found tA -> do unless (tA == t) (throwError $ errUnify e tA t)
+                   return θ
+    _        -> throwError $ errUnify e (FObj a) t
+
 --------------------------------------------------------------------------------
 -- | Checking Predicates -------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -805,7 +835,34 @@
 
 checkRelTy _ e _  t1 t2      = unless (t1 == t2) (throwError $ errRel e t1 t2)
 
+
+
 --------------------------------------------------------------------------------
+-- | Sort Unification on Expressions
+--------------------------------------------------------------------------------
+
+unifyExpr :: Env -> Expr -> Maybe TVSubst
+unifyExpr f (EApp e1 e2) = Just $ mconcat $ catMaybes [θ1, θ2, θ]
+  where
+   θ1 = unifyExpr f e1
+   θ2 = unifyExpr f e2
+   θ  = unifyExprApp f e1 e2
+unifyExpr f (ECst e _)
+  = unifyExpr f e
+unifyExpr _ _
+  = Nothing
+
+unifyExprApp :: Env -> Expr -> Expr -> Maybe TVSubst
+unifyExprApp f e1 e2 = do
+  t1 <- getArg $ exprSort_maybe e1
+  t2 <- exprSort_maybe e2
+  unify f (Just $ EApp e1 e2) t1 t2
+  where
+    getArg (Just (FFunc t1 _)) = Just t1
+    getArg _                   = Nothing
+
+
+--------------------------------------------------------------------------------
 -- | Sort Unification
 --------------------------------------------------------------------------------
 unify :: Env -> Maybe Expr -> Sort -> Sort -> Maybe TVSubst
@@ -880,12 +937,19 @@
 unify1 f e !θ (FFunc !t1 !t2) (FFunc !t1' !t2') = do
   unifyMany f e θ [t1, t2] [t1', t2']
 
+unify1 f e θ (FObj a) !t =
+  checkEqConstr f e θ a t
+
+unify1 f e θ !t (FObj a) =
+  checkEqConstr f e θ a t
+
 unify1 _ e θ !t1 !t2
   | t1 == t2
   = return θ
   | otherwise
   = throwError $ errUnify e t1 t2
 
+
 subst :: Int -> Sort -> Sort -> Sort
 subst !j !tj !t@(FVar !i)
   | i == j                  = tj
@@ -944,7 +1008,24 @@
     f t@(FVar i) = fromMaybe t (lookupVar i θ)
     f t          = t
 
+applyExpr :: Maybe TVSubst -> Expr -> Expr
+applyExpr Nothing e  = e
+applyExpr (Just θ) e = Vis.mapExpr f e
+  where
+    f (ECst e s) = ECst e (apply θ s)
+    f e          = e
+
 --------------------------------------------------------------------------------
+_applyCoercion :: Symbol -> Sort -> Sort -> Sort
+--------------------------------------------------------------------------------
+_applyCoercion a t = Vis.mapSort f
+  where
+    f (FObj b)
+      | a == b    = t
+    f s           = s
+
+
+--------------------------------------------------------------------------------
 -- | Deconstruct a function-sort -----------------------------------------------
 --------------------------------------------------------------------------------
 checkFunSort :: Sort -> CheckM (Sort, Sort, TVSubst)
@@ -961,6 +1042,10 @@
 
 newtype TVSubst = Th (M.HashMap Int Sort) deriving (Show)
 
+instance Monoid TVSubst where
+  mempty                  = Th mempty
+  mappend (Th s1) (Th s2) = Th (mappend s1 s2)
+
 lookupVar :: Int -> TVSubst -> Maybe Sort
 lookupVar i (Th m)   = M.lookup i m
 
@@ -979,11 +1064,11 @@
 
 errUnify :: Maybe Expr -> Sort -> Sort -> String
 errUnify eo t1 t2 = printf "Cannot unify %s with %s %s"
-                      (showpp t1) (showpp t2) (unifyExpr eo)
+                      (showpp t1) (showpp t2) (errUnifyExpr eo)
 
-unifyExpr :: Maybe Expr -> String
-unifyExpr Nothing  = ""
-unifyExpr (Just e) = "in expression: " ++ showpp e
+errUnifyExpr :: Maybe Expr -> String
+errUnifyExpr Nothing  = ""
+errUnifyExpr (Just e) = "in expression: " ++ showpp e
 
 errUnifyMany :: [Sort] -> [Sort] -> String
 errUnifyMany ts ts'  = printf "Cannot unify types with different cardinalities %s and %s"
diff --git a/src/Language/Fixpoint/Types/Config.hs b/src/Language/Fixpoint/Types/Config.hs
--- a/src/Language/Fixpoint/Types/Config.hs
+++ b/src/Language/Fixpoint/Types/Config.hs
@@ -56,41 +56,40 @@
 defaultMaxPartSize = 700
 
 
-data Config
-  = Config {
-      srcFile     :: FilePath            -- ^ src file (*.hs, *.ts, *.c, or even *.fq or *.bfq)
-    , cores       :: Maybe Int           -- ^ number of cores used to solve constraints
-    , minPartSize :: Int                 -- ^ Minimum size of a partition
-    , maxPartSize :: Int                 -- ^ Maximum size of a partition. Overrides minPartSize
-    , solver      :: SMTSolver           -- ^ which SMT solver to use
-    , linear      :: Bool                -- ^ not interpret div and mul in SMT
-    , stringTheory :: Bool               -- ^ interpretation of string theory by SMT
-    , defunction  :: Bool                -- ^ defunctionalize (use 'apply' for all uninterpreted applications)
-    , allowHO     :: Bool                -- ^ allow higher order binders in the logic environment
-    , allowHOqs   :: Bool                -- ^ allow higher order qualifiers
-    , eliminate   :: Eliminate           -- ^ eliminate non-cut KVars
-    , elimBound   :: Maybe Int           -- ^ maximum length of KVar chain to eliminate
-    , elimStats   :: Bool                -- ^ print eliminate stats
-    , solverStats :: Bool                -- ^ print solver stats
-    , metadata    :: Bool                -- ^ print meta-data associated with constraints
-    , stats       :: Bool                -- ^ compute constraint statistics
-    , parts       :: Bool                -- ^ partition FInfo into separate fq files
-    , save        :: Bool                -- ^ save FInfo as .bfq and .fq file
-    , minimize    :: Bool                -- ^ min .fq by delta debug (unsat with min constraints)
-    , minimizeQs  :: Bool                -- ^ min .fq by delta debug (sat with min qualifiers)
-    , minimizeKs  :: Bool                -- ^ min .fq by delta debug (sat with min kvars)
-    , minimalSol  :: Bool                -- ^ shrink final solution by pruning redundant qualfiers from fixpoint
-    , gradual     :: Bool                -- ^ solve "gradual" constraints
-    , ginteractive :: Bool                -- ^ interactive gradual solving
-    , extensionality   :: Bool           -- ^ allow function extensionality
-    , alphaEquivalence :: Bool           -- ^ allow lambda alpha equivalence axioms
-    , betaEquivalence  :: Bool           -- ^ allow lambda beta equivalence axioms
-    , normalForm       :: Bool           -- ^ allow lambda normal-form equivalence axioms
-    , autoKuts         :: Bool           -- ^ ignore given kut variables
-    , nonLinCuts       :: Bool           -- ^ Treat non-linear vars as cuts
-    , noslice          :: Bool           -- ^ Disable non-concrete KVar slicing
-    , rewriteAxioms    :: Bool           -- ^ allow axiom instantiation via rewriting
-    } deriving (Eq,Data,Typeable,Show,Generic)
+data Config = Config
+  { srcFile     :: FilePath            -- ^ src file (*.hs, *.ts, *.c, or even *.fq or *.bfq)
+  , cores       :: Maybe Int           -- ^ number of cores used to solve constraints
+  , minPartSize :: Int                 -- ^ Minimum size of a partition
+  , maxPartSize :: Int                 -- ^ Maximum size of a partition. Overrides minPartSize
+  , solver      :: SMTSolver           -- ^ which SMT solver to use
+  , linear      :: Bool                -- ^ not interpret div and mul in SMT
+  , stringTheory :: Bool               -- ^ interpretation of string theory by SMT
+  , defunction  :: Bool                -- ^ defunctionalize (use 'apply' for all uninterpreted applications)
+  , allowHO     :: Bool                -- ^ allow higher order binders in the logic environment
+  , allowHOqs   :: Bool                -- ^ allow higher order qualifiers
+  , eliminate   :: Eliminate           -- ^ eliminate non-cut KVars
+  , elimBound   :: Maybe Int           -- ^ maximum length of KVar chain to eliminate
+  , elimStats   :: Bool                -- ^ print eliminate stats
+  , solverStats :: Bool                -- ^ print solver stats
+  , metadata    :: Bool                -- ^ print meta-data associated with constraints
+  , stats       :: Bool                -- ^ compute constraint statistics
+  , parts       :: Bool                -- ^ partition FInfo into separate fq files
+  , save        :: Bool                -- ^ save FInfo as .bfq and .fq file
+  , minimize    :: Bool                -- ^ min .fq by delta debug (unsat with min constraints)
+  , minimizeQs  :: Bool                -- ^ min .fq by delta debug (sat with min qualifiers)
+  , minimizeKs  :: Bool                -- ^ min .fq by delta debug (sat with min kvars)
+  , minimalSol  :: Bool                -- ^ shrink final solution by pruning redundant qualfiers from fixpoint
+  , gradual     :: Bool                -- ^ solve "gradual" constraints
+  , ginteractive :: Bool                -- ^ interactive gradual solving
+  , extensionality   :: Bool           -- ^ allow function extensionality
+  , alphaEquivalence :: Bool           -- ^ allow lambda alpha equivalence axioms
+  , betaEquivalence  :: Bool           -- ^ allow lambda beta equivalence axioms
+  , normalForm       :: Bool           -- ^ allow lambda normal-form equivalence axioms
+  , autoKuts         :: Bool           -- ^ ignore given kut variables
+  , nonLinCuts       :: Bool           -- ^ Treat non-linear vars as cuts
+  , noslice          :: Bool           -- ^ Disable non-concrete KVar slicing
+  , rewriteAxioms    :: Bool           -- ^ allow axiom instantiation via rewriting
+  } deriving (Eq,Data,Typeable,Show,Generic)
 
 instance Default Config where
   def = defConfig
diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs
--- a/src/Language/Fixpoint/Types/Constraints.hs
+++ b/src/Language/Fixpoint/Types/Constraints.hs
@@ -55,7 +55,7 @@
   , FixSolution
   , GFixSolution, toGFixSol
   , Result (..)
-  , unsafe, isUnsafe, safe
+  , unsafe, isUnsafe, isSafe ,safe
 
   -- * Cut KVars
   , Kuts (..)
@@ -69,8 +69,8 @@
   -- * Axioms
   , AxiomEnv (..)
   , Equation (..)
+  , mkEquation
   , Rewrite  (..)
-  , getEqBody
 
   -- * Misc  [should be elsewhere but here due to dependencies]
   , substVars
@@ -142,6 +142,9 @@
 isGWfc (GWfC {}) = True
 isGWfc (WfC  {}) = False
 
+instance HasGradual (WfC a) where
+  isGradual = isGWfc
+
 type SubcId = Integer
 
 data SubC a = SubC
@@ -263,6 +266,10 @@
 unsafe = mempty {resStatus = Unsafe []}
 safe   = mempty {resStatus = Safe}
 
+isSafe :: Result a -> Bool
+isSafe (Result Safe _ _) = True
+isSafe _                 = False
+
 isUnsafe :: Result a -> Bool
 isUnsafe r | Unsafe _ <- resStatus r
   = True
@@ -602,6 +609,9 @@
      }
   deriving (Eq, Show, Functor, Generic)
 
+instance HasGradual (GInfo c a) where
+  isGradual info = any isGradual (M.elems $ ws info)
+
 instance Monoid HOInfo where
   mempty        = HOI False False
   mappend i1 i2 = HOI { hoBinds = hoBinds i1 || hoBinds i2
@@ -738,10 +748,11 @@
 ---------------------------------------------------------------------------
 -- | Axiom Instantiation Information --------------------------------------
 ---------------------------------------------------------------------------
-data AxiomEnv = AEnv { aenvEqs     :: ![Equation]
-                     , aenvSimpl   :: ![Rewrite]
-                     , aenvExpand  :: M.HashMap SubcId Bool
-                     }
+data AxiomEnv = AEnv
+  { aenvEqs     :: ![Equation]
+  , aenvSimpl   :: ![Rewrite]
+  , aenvExpand  :: M.HashMap SubcId Bool
+  }
   deriving (Eq, Show, Generic)
 
 instance B.Binary AxiomEnv
@@ -756,43 +767,64 @@
 instance NFData Eliminate
 
 instance Monoid AxiomEnv where
-  mempty = AEnv [] [] (M.fromList [])
-  mappend a1 a2 = AEnv aenvEqs' aenvSimpl' aenvExpand'
-    where aenvEqs'     = mappend (aenvEqs a1) (aenvEqs a2)
-          aenvSimpl'   = mappend (aenvSimpl a1) (aenvSimpl a2)
-          aenvExpand'  = mappend (aenvExpand a1) (aenvExpand a2)
+  mempty           = AEnv [] [] (M.fromList [])
+  mappend a1 a2    = AEnv aenvEqs' aenvSimpl' aenvExpand'
+    where
+      aenvEqs'     = mappend (aenvEqs a1) (aenvEqs a2)
+      aenvSimpl'   = mappend (aenvSimpl a1) (aenvSimpl a2)
+      aenvExpand'  = mappend (aenvExpand a1) (aenvExpand a2)
 
-data Equation = Equ { eqName :: Symbol
-                    , eqArgs :: [Symbol]
-                    , eqBody :: Expr
-                    }
+instance PPrint AxiomEnv where
+  pprintTidy _ = text . show
+
+data Equation = Equ
+  { eqName :: !Symbol           -- ^ name of reflected function
+  , eqArgs :: [(Symbol, Sort)]  -- ^ names of parameters
+  , eqBody :: !Expr             -- ^ definition of body
+  , eqSort :: !Sort             -- ^ sort of body
+  , eqRec  :: !Bool             -- ^ is this a recursive definition
+  }
   deriving (Eq, Show, Generic)
 
+mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
+mkEquation f xts e out = Equ f xts e out (f `elem` syms e)
+
+instance Subable Equation where
+  syms   a = syms (eqBody a) -- ++ F.syms (axiomEq a)
+  subst su = mapEqBody (subst su)
+  substf f = mapEqBody (substf f)
+  substa f = mapEqBody (substa f)
+
+mapEqBody :: (Expr -> Expr) -> Equation -> Equation
+mapEqBody f a = a { eqBody = f (eqBody a) }
+
 instance PPrint Equation where
-  pprintTidy k (Equ f xs e) = "def" <+> pprint f <+> intersperse " " (pprint <$> xs) <+> ":=" <+> pprintTidy k e
+  pprintTidy _ = toFix
 
+ppArgs :: (PPrint a) => [a] -> Doc
+ppArgs = parens . intersperse ", " . fmap pprint
 
 -- eg  SMeasure (f D [x1..xn] e)
 -- for f (D x1 .. xn) = e
-data Rewrite  = SMeasure  { smName  :: Symbol         -- eg. f
-                          , smDC    :: Symbol         -- eg. D
-                          , smArgs  :: [Symbol]       -- eg. xs
-                          , smBody  :: Expr           -- eg. e[xs]
-                          }
+data Rewrite  = SMeasure
+  { smName  :: Symbol         -- eg. f
+  , smDC    :: Symbol         -- eg. D
+  , smArgs  :: [Symbol]       -- eg. xs
+  , smBody  :: Expr           -- eg. e[xs]
+  }
   deriving (Eq, Show, Generic)
 
 instance Fixpoint AxiomEnv where
   toFix axe = vcat ((toFix <$> aenvEqs axe) ++ (toFix <$> aenvSimpl axe))
               $+$ text "expand" <+> toFix (pairdoc <$> M.toList(aenvExpand axe))
-    where pairdoc (x,y) = text $ show x ++ " : " ++ show y
+    where
+      pairdoc (x,y) = text $ show x ++ " : " ++ show y
 
 instance Fixpoint Doc where
   toFix = id
 
 instance Fixpoint Equation where
-  toFix (Equ f xs e)  = text "define"
-                     <+> toFix f <+> hsep (toFix <$> xs) <+> text " = "
-                     <+> lparen <> toFix e <> rparen
+  toFix (Equ f xs e _ _) = "define" <+> toFix f <+> ppArgs xs <+> text "=" <+> parens (toFix e)
 
 instance Fixpoint Rewrite where
   toFix (SMeasure f d xs e)
@@ -800,13 +832,7 @@
    <+> toFix f
    <+> parens (toFix d <+> hsep (toFix <$> xs))
    <+> text " = "
-   <+> lparen <> toFix e <> rparen
+   <+> parens (toFix e)
 
-getEqBody :: Equation -> Maybe Expr
-getEqBody (Equ  x xs (PAnd ((PAtom Eq fxs e):_)))
-  | (EVar f, es) <- splitEApp fxs
-  , f == x
-  , es == (EVar <$> xs)
-  = Just e
-getEqBody _
-  = Nothing
+instance PPrint Rewrite where
+  pprintTidy _ = toFix
diff --git a/src/Language/Fixpoint/Types/Names.hs b/src/Language/Fixpoint/Types/Names.hs
--- a/src/Language/Fixpoint/Types/Names.hs
+++ b/src/Language/Fixpoint/Types/Names.hs
@@ -214,8 +214,10 @@
 instance Fixpoint T.Text where
   toFix = text . T.unpack
 
--- RJ: Use `symbolSafeText` if you want it to machine-readable,
---     but `symbolText`     if you want it to be human-readable.
+{- | [NOTE: SymbolText]
+	Use `symbolSafeText` if you want it to machine-readable,
+        but `symbolText`     if you want it to be human-readable.
+ -}
 
 instance Fixpoint Symbol where
   toFix = toFix . checkedText -- symbolSafeText
@@ -603,6 +605,8 @@
         , mapConName
         , "Map_select"
         , "Map_store"
+        , "Map_union"
+        , "Map_default"
         , size32Name
         , size64Name
         , bitVecName
diff --git a/src/Language/Fixpoint/Types/Refinements.hs b/src/Language/Fixpoint/Types/Refinements.hs
--- a/src/Language/Fixpoint/Types/Refinements.hs
+++ b/src/Language/Fixpoint/Types/Refinements.hs
@@ -160,7 +160,9 @@
 class HasGradual a where
   isGradual :: a -> Bool
   gVars     :: a -> [KVar]
+  gVars _ = [] 
   ungrad    :: a -> a
+  ungrad x = x 
 
 instance HasGradual Expr where
   isGradual (PGrad {}) = True
@@ -278,6 +280,7 @@
           | PAll   ![(Symbol, Sort)] !Expr
           | PExist ![(Symbol, Sort)] !Expr
           | PGrad  !KVar !Subst !GradInfo !Expr
+          | ECoerc !Sort !Sort !Expr  
           deriving (Eq, Show, Data, Typeable, Generic)
 
 type Pred = Expr
@@ -339,7 +342,7 @@
     go (PExist _ e)    = go e
     go (PKVar _ _)     = 1
     go (PGrad _ _ _ e) = go e
-
+    go (ECoerc _ _ e)  = go e
 
 -- | Parsed refinement of @Symbol@ as @Expr@
 --   e.g. in '{v: _ | e }' v is the @Symbol@ and e the @Expr@
@@ -426,6 +429,7 @@
   toFix (ETApp e s)      = text "tapp" <+> toFix e <+> toFix s
   toFix (ETAbs e s)      = text "tabs" <+> toFix e <+> toFix s
   toFix (PGrad k _ _ e)  = toFix e <+> text "&&" <+> toFix k -- text "??" -- <+> toFix k <+> toFix su
+  toFix (ECoerc a t e)   = text "coerce" <+> toFix a <+> text "~" <+> toFix t <+> text "in" <+> toFix e -- text "??" -- <+> toFix k <+> toFix su
   toFix (ELam (x,s) e)   = text "lam" <+> toFix x <+> ":" <+> toFix s <+> "." <+> toFix e
 
   simplify (PAnd [])     = PTrue
@@ -594,6 +598,7 @@
   pprintPrec _ k (PAll xts p)    = pprintQuant k "forall" xts p
   pprintPrec _ k (PExist xts p)  = pprintQuant k "exists" xts p
   pprintPrec _ k (ELam (x,t) e)  = "lam" <+> toFix x <+> ":" <+> toFix t <+> text "." <+> pprintTidy k e
+  pprintPrec _ k (ECoerc a t e)  = parens $ "coerce" <+> toFix a <+> "~" <+> toFix t <+> text "in" <+> pprintTidy k e
   pprintPrec _ _ p@(PKVar {})    = toFix p
   pprintPrec _ _ (ETApp e s)     = "ETApp" <+> toFix e <+> toFix s
   pprintPrec _ _ (ETAbs e s)     = "ETAbs" <+> toFix e <+> toFix s
diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs
--- a/src/Language/Fixpoint/Types/Sorts.hs
+++ b/src/Language/Fixpoint/Types/Sorts.hs
@@ -53,7 +53,7 @@
   , mkFFunc
   , bkFFunc
 
-  , isNumeric, isReal, isString, isPolyInst 
+  , isNumeric, isReal, isString, isPolyInst
 
   -- * User-defined ADTs
   , DataField (..)
@@ -81,7 +81,10 @@
 
 
 data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic)
-type TCEmb a  = M.HashMap a FTycon
+type TCEmb a  = M.HashMap a Sort -- FTycon
+
+-- instance Show FTycon where
+--   show (TC s _) = show (val s)
 
 instance Symbolic FTycon where
   symbol (TC s _) = symbol s
diff --git a/src/Language/Fixpoint/Types/Spans.hs b/src/Language/Fixpoint/Types/Spans.hs
--- a/src/Language/Fixpoint/Types/Spans.hs
+++ b/src/Language/Fixpoint/Types/Spans.hs
@@ -16,10 +16,12 @@
 
   -- * Constructing spans
   , dummySpan
+  , panicSpan
   , locAt
   , dummyLoc
   , dummyPos
   , atLoc
+  , toSourcePos
 
   -- * Destructing spans
   , sourcePosElts
@@ -173,8 +175,11 @@
   srcSpan _ = dummySpan
 
 dummySpan :: SrcSpan
-dummySpan = SS l l
-  where l = initialPos ""
+dummySpan = panicSpan ""
+
+panicSpan :: String -> SrcSpan
+panicSpan s = SS l l
+  where l = initialPos s
 
 -- atLoc :: Located a -> b -> Located b
 -- atLoc (Loc l l' _) = Loc l l'
diff --git a/src/Language/Fixpoint/Types/Substitutions.hs b/src/Language/Fixpoint/Types/Substitutions.hs
--- a/src/Language/Fixpoint/Types/Substitutions.hs
+++ b/src/Language/Fixpoint/Types/Substitutions.hs
@@ -39,10 +39,10 @@
 
 mkSubst :: [(Symbol, Expr)] -> Subst
 
-mkSubst = Su . M.fromList . reverse . filter notTrivial 
+mkSubst = Su . M.fromList . reverse . filter notTrivial
   where
     notTrivial (x, EVar y) = x /= y
-    notTrivial _           = True  
+    notTrivial _           = True
 
 isEmptySubst :: Subst -> Bool
 isEmptySubst (Su xes) = M.null xes
@@ -108,6 +108,7 @@
   substa f                 = substf (EVar . f)
   substf f (EApp s e)      = EApp (substf f s) (substf f e)
   substf f (ELam x e)      = substfLam f x e
+  substf f (ECoerc a t e)  = ECoerc a t (substf f e)
   substf f (ENeg e)        = ENeg (substf f e)
   substf f (EBin op e1 e2) = EBin op (substf f e1) (substf f e2)
   substf f (EIte p e1 e2)  = EIte (substf f p) (substf f e1) (substf f e2)
@@ -127,6 +128,7 @@
 
   subst su (EApp f e)      = EApp (subst su f) (subst su e)
   subst su (ELam x e)      = ELam x (subst (removeSubst su (fst x)) e)
+  subst su (ECoerc a t e)  = ECoerc a t (subst su e)
   subst su (ENeg e)        = ENeg (subst su e)
   subst su (EBin op e1 e2) = EBin op (subst su e1) (subst su e2)
   subst su (EIte p e1 e2)  = EIte (subst su p) (subst su e1) (subst su e2)
@@ -268,6 +270,7 @@
     go (EVar x)           = [x]
     go (EApp f e)         = go f ++ go e
     go (ELam (x,_) e)     = filter (/= x) (go e)
+    go (ECoerc _ _ e)     = go e
     go (ENeg e)           = go e
     go (EBin _ e1 e2)     = go e1 ++ go e2
     go (EIte p e1 e2)     = exprSymbols p ++ go e1 ++ go e2
diff --git a/src/Language/Fixpoint/Types/Visitor.hs b/src/Language/Fixpoint/Types/Visitor.hs
--- a/src/Language/Fixpoint/Types/Visitor.hs
+++ b/src/Language/Fixpoint/Types/Visitor.hs
@@ -172,6 +172,7 @@
     step !c !(PAtom r e1 e2) = PAtom r     <$> vE c e1 <*> vE c e2
     step !c !(PAll xts p)    = PAll   xts  <$> vE c p
     step !c !(ELam (x,t) e)  = ELam (x,t)  <$> vE c e
+    step !c !(ECoerc a t e)  = ECoerc a t  <$> vE c e
     step !c !(PExist xts p)  = PExist xts  <$> vE c p
     step !c !(ETApp e s)     = (`ETApp` s) <$> vE c e
     step !c !(ETAbs e s)     = (`ETAbs` s) <$> vE c e
@@ -220,6 +221,7 @@
     go (ECst e t)      = f =<< ((`ECst` t)  <$>  go e                     )
     go (PAll xts p)    = f =<< (PAll   xts  <$>  go p                     )
     go (ELam (x,t) e)  = f =<< (ELam (x,t)  <$>  go e                     )
+    go (ECoerc a t e)  = f =<< (ECoerc a t  <$>  go e                     )
     go (PExist xts p)  = f =<< (PExist xts  <$>  go p                     )
     go (ETApp e s)     = f =<< ((`ETApp` s) <$>  go e                     )
     go (ETAbs e s)     = f =<< ((`ETAbs` s) <$>  go e                     )
diff --git a/tests/neg/maps.fq b/tests/neg/maps.fq
new file mode 100644
--- /dev/null
+++ b/tests/neg/maps.fq
@@ -0,0 +1,37 @@
+
+bind 1 m1 : {v : Map_t Int Int | v = Map_default 0}
+bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store m1 10 1) 20 1) } 
+bind 3 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 1) 10 1) } 
+bind 4 m4 : {v : Map_t Int Int | v = (Map_store m1 10 1) } 
+bind 5 m5 : {v : Map_t Int Int | v = (Map_store m1 20 1) } 
+
+constraint:
+  env [ 1 ]
+  lhs {v : int | v = Map_select m1 100 }
+  rhs {v : int | v = 0 } 
+  id 1 tag []
+
+constraint:
+  env [ 1; 2 ]
+  lhs {v : int | v = Map_select m2 100 }
+  rhs {v : int | v = 0 } 
+  id 2 tag []
+
+constraint:
+  env [ 1; 2 ]
+  lhs {v : int | v = Map_select m2 10 }
+  rhs {v : int | v = 1 } 
+  id 3 tag []
+
+constraint:
+  env [ 1; 2; 3 ]
+  lhs {v : int | true }
+  rhs {v : int | m2 = m3 } 
+  id 4 tag []
+
+constraint:
+  env [ 1; 2; 3; 4; 5 ]
+  lhs {v : int | true }
+  rhs {v : int | m2 = Map_union m4 m4 } 
+  id 5 tag []
+
diff --git a/tests/pos/EqConstr0.fq b/tests/pos/EqConstr0.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/EqConstr0.fq
@@ -0,0 +1,10 @@
+ 
+bind 0 a : {v: int | true } 
+bind 1 x : {v: int | true } 
+bind 2 y : {v: a   | true } 
+
+constraint:  
+  env [0; 1; 2]
+  lhs {v: int | x = y }
+  rhs {v: Int | y = x }
+  id 1 tag []
diff --git a/tests/pos/EqConstr1.fq b/tests/pos/EqConstr1.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/EqConstr1.fq
@@ -0,0 +1,13 @@
+data Thing 0 = [
+  | mkCons { head : int } 
+]
+  
+bind 0 a : {v: Thing | true } 
+bind 1 x : {v: Thing | true } 
+bind 2 y : {v: a     | true } 
+
+constraint:  
+  env [0; 1; 2]
+  lhs {v: int | x = y }
+  rhs {v: Int | y = x }
+  id 1 tag []
diff --git a/tests/pos/adt_pair_cast.fq b/tests/pos/adt_pair_cast.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/adt_pair_cast.fq
@@ -0,0 +1,13 @@
+
+data P 2 = [
+   | P {pfst : @(0), psnd : @(1)}
+   ]
+
+bind 1 pig : {v : int  | true }
+bind 2 dog : {v : bool | true }
+
+constraint:
+  env [1;2]
+  lhs {v : int | psnd (P pig dog) }
+  rhs {v:int | 12 = 4 + 8}
+  id 1 tag []
diff --git a/tests/pos/coerce0.fq b/tests/pos/coerce0.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/coerce0.fq
@@ -0,0 +1,12 @@
+constant f : (func(1, [(Foo int); int]))
+
+bind 1 pig : {v : (Foo a) | true }
+
+bind 2 dog : {v : int | v = f (coerce (Foo a ~ Foo int) pig) }
+
+
+constraint:
+  env [1;2]
+  lhs {v : int | v = 10 }
+  rhs {v : int | v = 5 + 5}
+  id 1 tag []
diff --git a/tests/pos/coerce1.fq b/tests/pos/coerce1.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/coerce1.fq
@@ -0,0 +1,11 @@
+constant f : (func(1, [(Foo int); int]))
+
+bind 1 pig : {v : (Foo a) | true }
+
+bind 2 dog : {v : int | v = f (coerce (Foo a ~ Foo int) pig) }
+
+constraint:
+  env [1;2]
+  lhs {v : int | v = 10 }
+  rhs {v : int | v = 5 + 5}
+  id 1 tag []
diff --git a/tests/pos/empty.fq b/tests/pos/empty.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/empty.fq
@@ -0,0 +1,13 @@
+// Config {srcFile = "/Users/rjhala/research/stack/liquidhaskell/tests/pos/lit00.hs", cores = Nothing, minPartSize = 500, maxPartSize = 700, solver = z3, linear = False, stringTheory = False, defunction = False, allowHO = False, allowHOqs = False, eliminate = some, elimBound = Nothing, elimStats = False, solverStats = False, metadata = False, stats = False, parts = False, save = True, minimize = False, minimizeQs = False, minimizeKs = False, minimalSol = False, gradual = False, ginteractive = False, extensionality = False, alphaEquivalence = False, betaEquivalence = False, normalForm = False, autoKuts = False, nonLinCuts = True, noslice = False, rewriteAxioms = True, arithmeticAxioms = False}
+
+constant Zero : (Peano) 
+constant One  : (Peano) 
+
+distinct Zero : (Peano) 
+distinct One  : (Peano) 
+
+
+bind 0 xZero : {v : Peano | v = Zero } 
+bind 1 xOne  : {v : Peano | v = One  } 
+
+
diff --git a/tests/pos/maps.fq b/tests/pos/maps.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/maps.fq
@@ -0,0 +1,37 @@
+
+bind 1 m1 : {v : Map_t Int Int | v = Map_default 0}
+bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store m1 10 1) 20 1) } 
+bind 3 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 1) 10 1) } 
+bind 4 m4 : {v : Map_t Int Int | v = (Map_store m1 10 1) } 
+bind 5 m5 : {v : Map_t Int Int | v = (Map_store m1 20 1) } 
+
+constraint:
+  env [ 1 ]
+  lhs {v : int | v = Map_select m1 100 }
+  rhs {v : int | v = 0 } 
+  id 1 tag []
+
+constraint:
+  env [ 1; 2 ]
+  lhs {v : int | v = Map_select m2 100 }
+  rhs {v : int | v = 0 } 
+  id 2 tag []
+
+constraint:
+  env [ 1; 2 ]
+  lhs {v : int | v = Map_select m2 10 }
+  rhs {v : int | v = 1 } 
+  id 3 tag []
+
+constraint:
+  env [ 1; 2; 3 ]
+  lhs {v : int | true }
+  rhs {v : int | m2 = m3 } 
+  id 4 tag []
+
+constraint:
+  env [ 1; 2; 3; 4; 5 ]
+  lhs {v : int | true }
+  rhs {v : int | m2 = Map_union m4 m5 } 
+  id 5 tag []
+
diff --git a/tests/testParser.hs b/tests/testParser.hs
--- a/tests/testParser.hs
+++ b/tests/testParser.hs
@@ -106,6 +106,10 @@
 
     , testCase "FObj " $
         show (doParse' sortP "test" "_foo") @?= "FObj \"_foo\""
+
+    , testCase "Coerce0" $
+        show (doParse' predP "test" "v = (coerce (a ~ int) (f x))")
+          @?= "PAtom Eq (EVar \"v\") (ECoerc (FObj \"a\") FInt (EApp (EVar \"f\") (EVar \"x\")))"
     ]
 
 -- ---------------------------------------------------------------------