diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md
index a8c96fb9f..f4d06a87b 100644
--- a/docs/mkDocs/docs/options.md
+++ b/docs/mkDocs/docs/options.md
@@ -132,8 +132,8 @@ you can assume the reflection of both functions by defining a *pretended* functi
 as the actual function. Therein lies the assumption: if both functions don't actually behave in the same way, then you
 may introduce falsity in your logic. Thus, you have to use it with caution, only when the function wasn't already reflected,
 and when you actually know how it will behave. In the following snippet, `myfilter` is the pretended function whose definition
-is given in our module, and the actual function `GHC.List.filter` and `myfilter` and tied through 
-the `{-@ assume reflect filter as myfilter @-}` annotation. This annotation must be read as: "reflect `filter`, assuming it has the 
+is given in our module, and the actual function `GHC.List.filter` and `myfilter` and tied through
+the `{-@ assume reflect filter as myfilter @-}` annotation. This annotation must be read as: "reflect `filter`, assuming it has the
 same reflection as `myfilter`".
 
 ```Haskell
@@ -390,6 +390,29 @@ the error. If you don't want the above and instead, want only the
 By default, the inferred types will have fully qualified module names.
 To use unqualified names, much easier to read, use `--short-names`.
 
+## Logical aliasing
+
+**Directives:** `define`
+
+You can force LiquidHaskell to treat each occurrence of a Haskell name (such as
+a function or a data constructor) as a predefined logical expression with the
+`define` directive. This can be useful for treating Haskell system functions
+as  no-ops, or for linking operations on your datatypes directly to SMT theories.
+
+As an example,
+
+```haskell
+{-@ define foo x y = (Foo_t y) @-}
+```
+
+will replace every occurrence of a Haskell symbol `foo` applied to two arguments
+with a logical symbol `Foo_t` applied to only the second argument, when processing
+specifications. The symbol `foo` can either be defined in the current module or
+imported, and the defined alias is propagated to the dependencies.
+
+See `Language.Haskell.Liquid.Bag` and `Language.Haskell.Liquid.ProofCombinators`
+for examples.
+
 ## Disabling Checks on Functions
 
 **Directives:** `ignore`
@@ -444,18 +467,18 @@ See the [specifications section](specifications.md) for how to write termination
 ## Positivity Check
 
 **Options:** `no-positivity-check`
-By **default** a positivity check is performed on data definitions. 
+By **default** a positivity check is performed on data definitions.
 
 
 ```haskell
-data Bad = Bad (Bad -> Bad) | Good Bad 
+data Bad = Bad (Bad -> Bad) | Good Bad
     --           A      B           C
     -- A is in a negative position, B and C are OK
 ```
 
 Negative declarations are rejected because they admit non-terminating functions.
 
-If the positivity check is disabled, so that a similar declaration of `Bad` is allowed, 
+If the positivity check is disabled, so that a similar declaration of `Bad` is allowed,
 it is possible to construct a term of the empty type, even without recursion.
 For example see [tests/neg/Positivity1.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/errors/Positivity1.hs)
 and [tests/neg/Positivity2.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/errors/Positivity2.hs)
diff --git a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
index ba05db986..e5dc09f93 100644
--- a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
+++ b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
@@ -19,44 +19,50 @@ import qualified Data.Map      as M
 data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
 
 {-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+{-@ define empty                = (Bag_empty 0) @-}
 empty :: Bag k
 empty = Bag M.empty
 
 {-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count b k}  @-}
+{-@ define get               k      b                    = (Bag_count b k) @-}
 get :: (Ord k) => k -> Bag k -> Int
 get k b = M.findWithDefault 0 k (toMap b)
 
 {-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Bag_union b (Bag_sng k 1)} @-}
-{-@ ignore put @-}
+{-@ define put               k      b                      = (Bag_union b (Bag_sng k 1)) @-}
 put :: (Ord k) => k -> Bag k -> Bag k
 put k b = Bag (M.insert k (1 + get k b) (toMap b))
 
-{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-}
-fromList :: (Ord k) => [k] -> Bag k
-fromList []     = empty
-fromList (x:xs) = put x (fromList xs)
-
-{-@ assume union :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Bag_union m1 m2} @-}
+{-@ assume union :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union a b} @-}
+{-@ define union               a          b                      = (Bag_union a b) @-}
 union :: (Ord k) => Bag k -> Bag k -> Bag k
 union b1 b2 = Bag (M.unionWith (+) (toMap b1) (toMap b2))
 
-{-@ assume unionMax :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Bag_union_max m1 m2} @-}
+{-@ assume unionMax :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union_max a b} @-}
+{-@ define unionMax               a          b                      = (Bag_union_max a b) @-}
 unionMax :: (Ord k) => Bag k -> Bag k -> Bag k
 unionMax b1 b2 = Bag (M.unionWith max (toMap b1) (toMap b2))
 
-{-@ assume interMin :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Bag_inter_min m1 m2} @-}
+{-@ assume interMin :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_inter_min a b} @-}
+{-@ define interMin               a          b                      = (Bag_inter_min a b) @-}
 interMin :: (Ord k) => Bag k -> Bag k -> Bag k
 interMin b1 b2 = Bag (M.intersectionWith min (toMap b1) (toMap b2))
 
-{-@ assume sub :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bool | v = Bag_sub m1 m2} @-}
+{-@ assume sub :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bool | v = Bag_sub a b} @-}
+{-@ define sub               a          b                     = (Bag_sub a b) @-}
 sub :: (Ord k) => Bag k -> Bag k -> Bool
 sub b1 b2 = M.isSubmapOfBy (<=) (toMap b1) (toMap b2)
 
+{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-}
+fromList :: (Ord k) => [k] -> Bag k
+fromList []     = empty
+fromList (x:xs) = put x (fromList xs)
+
 {-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}
 bagSize :: Bag k -> Int
 bagSize b = sum (M.elems (toMap b))
 
-{-@ thm_emp :: x:k -> xs:Bag k -> { Language.Haskell.Liquid.Bag.empty /= put x xs } @-}
+{-@ thm_emp :: x:k -> xs:Bag k -> { empty /= put x xs } @-}
 thm_emp :: (Ord k) => k -> Bag k -> ()
 thm_emp x xs = const () (get x xs)
 
diff --git a/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs b/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs
index 9faf8d614..7774cdd23 100644
--- a/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs
+++ b/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs
@@ -10,7 +10,7 @@ module Language.Haskell.Liquid.ProofCombinators (
 
   -- * Proof is just a () alias
   Proof
-  , toProof 
+  , toProof
 
   -- * Proof constructors
   , trivial, unreachable, (***), QED(..)
@@ -21,18 +21,18 @@ module Language.Haskell.Liquid.ProofCombinators (
   -- * These two operators check all intermediate equalities
   , (===) -- proof of equality is implicit eg. x === y
   , (=<=) -- proof of equality is implicit eg. x <= y
-  , (=>=)  -- proof of equality is implicit eg. x =>= y 
+  , (=>=)  -- proof of equality is implicit eg. x =>= y
 
   -- * This operator does not check intermediate equalities
-  , (==.) 
+  , (==.)
 
   -- Uncheck operator used only for proof debugging
   , (==!) -- x ==! y always succeeds
 
   -- * Combining Proofs
   , (&&&)
-  , withProof 
-  , impossible 
+  , withProof
+  , impossible
 
   -- * PLE-specific
   , pleUnfold
@@ -120,9 +120,9 @@ _ =>= y  = y
 infixl 3 ?
 
 {-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
-(?) :: a -> b -> a 
-x ? _ = x 
-{-# INLINE (?)   #-} 
+(?) :: a -> b -> a
+x ? _ = x
+{-# INLINE (?)   #-}
 
 -------------------------------------------------------------------------------
 -- | Assumed equality
@@ -149,13 +149,13 @@ infixl 3 ==!
 -- | The above operators check each intermediate proof step.
 --   The operator `==.` below accepts an optional proof term
 --   argument, but does not check intermediate steps.
---   So, using `==.` the proofs are faster, but the error messages worse. 
+--   So, using `==.` the proofs are faster, but the error messages worse.
 
 infixl 3 ==.
 
-{-# INLINE (==.) #-} 
-(==.) :: a -> a -> a 
-_ ==. x = x 
+{-# INLINE (==.) #-}
+(==.) :: a -> a -> a
+_ ==. x = x
 
 -------------------------------------------------------------------------------
 -- | * Combining Proof Certificates -------------------------------------------
@@ -165,7 +165,8 @@ _ ==. x = x
 x &&& _ = x
 
 
-{-@ withProof :: x:a -> b -> {v:a | v = x} @-}
+{-@        withProof :: x:a -> b -> {v:a | v = x} @-}
+{-@ define withProof    x      y            = (x) @-}
 withProof :: a -> b -> a
 withProof x _ = x
 
@@ -174,7 +175,7 @@ impossible :: a -> b
 impossible _ = undefined
 
 -------------------------------------------------------------------------------
--- | Convenient Syntax for Inductive Propositions 
+-- | Convenient Syntax for Inductive Propositions
 -------------------------------------------------------------------------------
 
 {-@ measure prop :: a -> b           @-}
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index b7b4bfc0e..16eb422a2 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -283,6 +283,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
                 , cmeasures  = mconcat $ map Ms.cmeasures $ map snd dependencySpecs ++ [targetSpec]
                 , embeds = Ms.embeds targetSpec
                 , privateReflects = mconcat $ map (privateReflects . snd) mspecs
+                , defines = Ms.defines targetSpec
                 }
     })
   where
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
index 93e80a3a0..b7d766731 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
@@ -553,7 +553,7 @@ checkAbstractRefs rt = go rt
 
 checkReft                    :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r)))
                              => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc
-checkReft _ _   _   Nothing _   = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.
+checkReft _  _   _   Nothing  _ = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.
 checkReft sp env emb (Just t) _ = (\z -> dr $+$ z) <$> checkSortedReftFull sp env r
   where
     r                           = rTypeSortedReft emb t
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index 5abfd4282..0ab6d1ecf 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -387,7 +387,7 @@ getLocReflects = S.unions . map names . M.elems
 -- Get all the symbols that are defined in the logic, based on the environment and the specs.
 -- Also, fully qualify the defined symbols by the way (for those for which it's possible and not already done).
 getDefinedSymbolsInLogic :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs -> S.HashSet F.LocSymbol
-getDefinedSymbolsInLogic env measEnv specs = 
+getDefinedSymbolsInLogic env measEnv specs =
   S.unions (uncurry getFromAxioms <$> specsList) -- reflections that ended up in equations
     `S.union` getLocReflects specs -- reflected symbols
     `S.union` measVars -- Get the data constructors, ex. for Lit00.0
@@ -472,7 +472,7 @@ getUnfoldingOfVar = getExpr . Ghc.realUnfoldingInfo . Ghc.idInfo
 -- For this purpose, you need to give the variable naming the definition to reflect
 -- and its corresponding equation in the logic.
 getFreeVarsOfReflectionOfVar  :: Ghc.Var -> F.Equation -> S.HashSet Ghc.Var
-getFreeVarsOfReflectionOfVar var eq = 
+getFreeVarsOfReflectionOfVar var eq =
     S.filter (\v -> F.symbol v `S.member` freeSymbolsInReflectedBody) freeVarsInCoreExpr
   where
     reflExpr = getUnfoldingOfVar var
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
index 34164cd7c..2a74678fc 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
@@ -2,52 +2,13 @@ module Language.Haskell.Liquid.GHC.CoreToLogic where
 
 coreToLogic :: String
 coreToLogic = unlines
-  [ "define Data.Set.Base.singleton x      = (Set_sng x)"
-  , "define Data.Set.Base.union x y        = (Set_cup x y)"
-  , "define Data.Set.Base.intersection x y = (Set_cap x y)"
-  , "define Data.Set.Base.difference x y   = (Set_dif x y)"
-  , "define Data.Set.Base.empty            = (Set_empty 0)"
-  , "define Data.Set.Base.null x           = (Set_emp x)"
-  , "define Data.Set.Base.member x xs      = (Set_mem x xs)"
-  , "define Data.Set.Base.isSubsetOf x y   = (Set_sub x y)"
-  , "define Data.Set.Base.fromList xs      = (listElts xs)"
-  , ""
-  , "define Data.Set.Internal.singleton x      = (Set_sng x)"
-  , "define Data.Set.Internal.union x y        = (Set_cup x y)"
-  , "define Data.Set.Internal.intersection x y = (Set_cap x y)"
-  , "define Data.Set.Internal.difference x y   = (Set_dif x y)"
-  , "define Data.Set.Internal.empty            = (Set_empty 0)"
-  , "define Data.Set.Internal.null x           = (Set_emp x)"
-  , "define Data.Set.Internal.member x xs      = (Set_mem x xs)"
-  , "define Data.Set.Internal.isSubsetOf x y   = (Set_sub x y)"
-  , "define Data.Set.Internal.fromList xs      = (Data.Set_LHAssumptions.listElts xs)"
-  , ""
-  , "define GHC.Internal.Real.fromIntegral x = (x)"
-  , ""
-  , "define GHC.Types.True                 = (true)"
-  , "define GHC.Internal.Real.div x y      = (x / y)"
-  , "define GHC.Internal.Real.mod x y      = (x mod y)"
-  , "define GHC.Internal.Num.fromInteger x = (x)"
-  , "define GHC.Num.Integer.IS x           = (x)"
-  , "define GHC.Classes.not x              = (~ x)"
-  , "define GHC.Internal.Base.$ f x        = (f x)"
-  , ""
-  , "define Language.Haskell.Liquid.Bag.get k b      = (Bag_count b k)"
-  , "define Language.Haskell.Liquid.Bag.put k b      = (Bag_union b (Bag_sng k 1))"
-  , "define Language.Haskell.Liquid.Bag.union a b    = (Bag_union a b)"
-  , "define Language.Haskell.Liquid.Bag.unionMax a b = (Bag_union_max a b)"
-  , "define Language.Haskell.Liquid.Bag.interMin a b = (Bag_inter_min a b)"
-  , "define Language.Haskell.Liquid.Bag.sub a b      = (Bag_sub a b)"
-  , "define Language.Haskell.Liquid.Bag.empty        = (Bag_empty 0)"
-  , ""
+  [ "define GHC.Types.True                   = (true)"
+  , "define GHC.Classes.not x                = (~ x)"
+  , "define GHC.Internal.Base.$ f x          = (f x)"
   , "define Main.mempty       = (mempty)"
-  , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
-  , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
-  , "define ProofCombinators.cast x y = (y)"
-  , "define Liquid.ProofCombinators.cast x y = (y)"
   , "define Control.Parallel.Strategies.withStrategy s x = (x)"
-  , ""
   , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
-  , ""
-  , "define GHC.CString.unpackCString# x = x"
+  , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
+  , "define Liquid.ProofCombinators.cast x y = (y)"
+  , "define ProofCombinators.cast x y = (y)"
   ]
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs
index 9c4d82b37..67c7e2fc4 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -274,8 +274,8 @@ makeLogicMap = do
     Right lm -> return (lm <> listLMap)
 
 listLMap :: LogicMap -- TODO-REBARE: move to wiredIn
-listLMap  = toLogicMap [ (dummyLoc nilName , []     , hNil)
-                       , (dummyLoc consName, [x, xs], hCons (EVar <$> [x, xs])) ]
+listLMap  = toLogicMap [ (dummyLoc nilName , ([]     , hNil))
+                       , (dummyLoc consName, ([x, xs], hCons (EVar <$> [x, xs]))) ]
   where
     x     = "x"
     xs    = "xs"
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 7f23c5e5e..ddebec0a3 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -19,11 +19,12 @@ import qualified Liquid.GHC.API         as O
 import           Liquid.GHC.API         as GHC hiding (Type)
 import qualified Text.PrettyPrint.HughesPJ               as PJ
 import qualified Language.Fixpoint.Types                 as F
-import qualified  Language.Haskell.Liquid.GHC.Misc        as LH
+import qualified Language.Haskell.Liquid.GHC.Misc        as LH
 import qualified Language.Haskell.Liquid.UX.CmdLine      as LH
 import qualified Language.Haskell.Liquid.GHC.Interface   as LH
 import           Language.Haskell.Liquid.LHNameResolution (resolveLHNames)
 import qualified Language.Haskell.Liquid.Liquid          as LH
+import qualified Language.Haskell.Liquid.Types.Names     as LH
 import qualified Language.Haskell.Liquid.Types.PrettyPrint as LH ( filterReportErrors
                                                                  , filterReportErrorsWith
                                                                  , defaultFilterReporter
@@ -286,7 +287,6 @@ typecheckHook cfg0 ms tcGblEnv = swapBreadcrumb thisModule Nothing >>= \case
   where
     thisModule = ms_mod ms
 
-
 typecheckHook' :: Config -> ModSummary -> TcGblEnv -> [SpecComment] -> TcM (Either LiquidCheckException TcGblEnv)
 typecheckHook' cfg ms tcGblEnv specComments = do
   debugLog $ "We are in module: " <> show (toStableModule thisModule)
@@ -543,25 +543,31 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
+        -- add defines from dependencies to the logical map
+        logicMapWithDeps =
+          foldr (\ls lmp ->
+                     lmp <> mkLogicMap (HM.map (fmap LH.lhNameToResolvedSymbol) $ liftedDefines ls))
+                lhModuleLogicMap $
+            (HM.elems . getDependencies) dependencies
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule
           localVars
           (imp_mods $ tcg_imports tcg)
           (tcg_rdr_env tcg)
-          lhModuleLogicMap
+          logicMapWithDeps
           bareSpec0
           dependencies
     result <-
       case eBareSpec of
         Left errors -> pure $ Left $ mkDiagnostics [] errors
-        Right (bareSpec, lnameEnv) ->
+        Right (bareSpec, lnameEnv, lmap') ->
           fmap (,bareSpec) <$>
             makeTargetSpec
               moduleCfg
               localVars
               lnameEnv
-              lhModuleLogicMap
+              lmap'
               targetSrc
               bareSpec
               dependencies
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index 96bec9bdf..f014ea7e3 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -137,9 +137,9 @@ resolveLHNames
   -> LogicMap
   -> BareSpecParsed
   -> TargetDependencies
-  -> Either [Error] (BareSpec, LogicNameEnv)
+  -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
 resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 dependencies = do
-    let ((bs, logicNameEnv), (es, ns)) =
+    let ((bs, logicNameEnv, lmap2), (es, ns)) =
           flip runState mempty $ do
             -- A generic traversal that resolves names of Haskell entities
             sp1 <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) $
@@ -152,27 +152,37 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
 
             (es0,_) <- get
             if null es0 then do
+
               -- Now we do a second traversal to resolve logic names
               let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
                     makeLogicEnvs impMods thisModule sp2 dependencies
+              -- Add resolved local defines to the logic map
+                  lmap1 =
+                    lmap <> mkLogicMap (HM.fromList $
+                                         (\(k , v) ->
+                                             let k' = lhNameToResolvedSymbol <$> k in
+                                             (F.val k', (val <$> v) { lmVar = k' }))
+                                         <$> defines sp2)
               sp3 <- fromBareSpecLHName <$>
                        resolveLogicNames
                          cfg
                          inScopeEnv
                          globalRdrEnv
                          unhandledNames
-                         lmap
+                         lmap1
                          localVars
                          logicNameEnv0
                          privateReflectNames
                          allEaliases
                          sp2
-              return (sp3, logicNameEnv0)
+              return (sp3, logicNameEnv0, lmap1)
             else
-              return (error "resolveLHNames: invalid spec", error "resolveLHNames: invalid logic environment")
+              return ( error "resolveLHNames: invalid spec"
+                     , error "resolveLHNames: invalid logic environment"
+                     , error "resolveLHNames: invalid logic map")
         logicNameEnv' = extendLogicNameEnv logicNameEnv ns
     if null es then
-      Right (bs, logicNameEnv')
+      Right (bs, logicNameEnv', lmap2)
     else
       Left es
   where
@@ -184,30 +194,32 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
         LHNUnresolved LHLogicNameBinder s -> pure $ makeLogicLHName s thisModule Nothing
         _ -> panic Nothing $ "unexpected name: " ++ show n
 
-    resolveLHName lname = case val lname of
-      LHNUnresolved LHTcName s
-        | isTuple s ->
-          pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
-        | isList s ->
-          pure $ LHNResolved (LHRGHC GHC.listTyConName) s
-        | s == "*" ->
-          pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s
-        | otherwise ->
-          case HM.lookup s taliases of
-            Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m Nothing) s
-            Nothing -> lookupGRELHName LHTcName lname s listToMaybe
-      LHNUnresolved ns@(LHVarName lcl) s
-        | isDataCon s -> lookupGRELHName (LHDataConName lcl) lname s listToMaybe
-        | otherwise ->
-            lookupGRELHName ns lname s
-              (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))
-      LHNUnresolved LHLogicNameBinder s ->
-        pure $ makeLogicLHName s thisModule Nothing
-      n@(LHNUnresolved LHLogicName _) ->
-        -- This one will be resolved by resolveLogicNames
-        pure n
-      LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe
-      n -> pure n
+    resolveLHName lname =
+      case val lname of
+        LHNUnresolved LHTcName s
+          | isTuple s ->
+            pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
+          | isList s ->
+            pure $ LHNResolved (LHRGHC GHC.listTyConName) s
+          | s == "*" ->
+            pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s
+          | otherwise ->
+            case HM.lookup s taliases of
+              Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m Nothing) s
+              Nothing -> lookupGRELHName LHTcName lname s listToMaybe
+        LHNUnresolved ns@(LHVarName lcl) s
+          | isDataCon s ->
+              lookupGRELHName (LHDataConName lcl) lname s listToMaybe
+          | otherwise ->
+              lookupGRELHName ns lname s
+                (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))
+        LHNUnresolved LHLogicNameBinder s ->
+          pure $ makeLogicLHName s thisModule Nothing
+        n@(LHNUnresolved LHLogicName _) ->
+          -- This one will be resolved by resolveLogicNames
+          pure n
+        LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe
+        n -> pure n
 
     lookupGRELHName ns lname s localNameLookup =
       case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index db920b756..cb813b4c4 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -191,13 +191,13 @@ toLogicP :: Parser LogicMap
 toLogicP
   = toLogicMap <$> many toLogicOneP
 
-toLogicOneP :: Parser  (LocSymbol, [Symbol], Expr)
+toLogicOneP :: Parser (LocSymbol, ([Symbol], Expr))
 toLogicOneP
   = do reserved "define"
        (x:xs) <- some locSymbolP
        reservedOp "="
        e      <- exprP <|> predP
-       return (x, val <$> xs, fmap val e)
+       return (x, (val <$> xs, val <$> e))
 
 
 --------------------------------------------------------------------------------
@@ -931,7 +931,7 @@ data BPspec
   | Varia   (Located LHName, [Variance])                  -- ^ 'variance' annotations, marking type constructor params as co-, contra-, or in-variant
   | DSize   ([LocBareTypeParsed], LocSymbol)              -- ^ 'data size' annotations, generating fancy termination metric
   | BFix    ()                                            -- ^ fixity annotation
-  | Define  (LocSymbol, Symbol)                           -- ^ 'define' annotation for specifying aliases c.f. `include-CoreToLogic.lg`
+  | Define  (Located LHName, ([Symbol], ExprV LocSymbol)) -- ^ 'define' annotation for specifying logic aliases
   deriving (Data, Typeable)
 
 instance PPrint BPspec where
@@ -1021,7 +1021,7 @@ ppPspec _ (Pragma  (Loc _ _ s))
 ppPspec k (CMeas   m)
   = "class measure" <+> pprintTidy k (unLocMeasureV m)
 ppPspec k (IMeas   m)
-  = "instance  measure" <+> pprintTidy k (val <$> unLocMeasureV m)
+  = "instance measure" <+> pprintTidy k (val <$> unLocMeasureV m)
 ppPspec k (Class   cls)
   = pprintTidy k $ fmap (fmap parsedToBareType) cls
 ppPspec k (RInst   inst)
@@ -1032,8 +1032,8 @@ ppPspec k (DSize   (ds, ss))
   = "data size" <+> splice " " (pprintTidy k <$> map (fmap parsedToBareType) ds) <+> pprintTidy k (val ss)
 ppPspec _ (BFix    _)           --
   = "fixity"
-ppPspec k (Define  (lx, y))
-  = "define" <+> pprintTidy k (val lx) <+> "=" <+> pprintTidy k y
+ppPspec k (Define  (lx, (ys, e)))
+  = "define" <+> pprintTidy k (val lx) <+> " " <+> pprintTidy k ys <+> "=" <+> pprintTidy k e
 ppPspec k (Relational (lxl, lxr, tl, tr, q, p))
   = "relational"
         <+> pprintTidy k (val lxl) <+> "::" <+> pprintTidy k (parsedToBareType <$> tl) <+> "~"
@@ -1133,6 +1133,7 @@ mkSpec xs = Measure.Spec
   , Measure.ignores    = S.fromList [s | Ignore s <- xs]
   , Measure.autosize   = S.fromList [s | ASize  s <- xs]
   , Measure.axeqs      = []
+  , Measure.defines    = [ toLMapV d | Define d <- xs]
   }
 
 -- | Parse a single top level liquid specification
@@ -1150,7 +1151,8 @@ specP
     <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP  )
     <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP  )
 
-    <|> fallbackSpecP "measure"    hmeasureP
+    <|> fallbackSpecP "define"  logDefineP
+    <|> fallbackSpecP "measure" hmeasureP
 
     <|> (reserved "infixl"        >> fmap BFix    infixlP  )
     <|> (reserved "infixr"        >> fmap BFix    infixrP  )
@@ -1327,6 +1329,14 @@ rtAliasP f bodyP
        let (tArgs, vArgs) = partition (isSmall . headSym) args
        return $ Loc pos posE (RTA name (f <$> tArgs) vArgs body)
 
+logDefineP :: Parser BPspec
+logDefineP =
+    do s <- locBinderLHNameP
+       args <- many locSymbolP
+       reservedOp "="
+       e <- exprP <|> predP
+       return (Define (s, (val <$> args, e)))
+
 hmeasureP :: Parser BPspec
 hmeasureP = do
   setLayout
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index 7747477c4..f7e640800 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -44,7 +44,7 @@ import GHC.Generics
 import GHC.Show
 import GHC.Stack
 import Language.Fixpoint.Types
-import Language.Haskell.Liquid.GHC.Misc (locNamedThing) -- Symbolic GHC.Name
+import Language.Haskell.Liquid.GHC.Misc ( locNamedThing ) -- Symbolic GHC.Name
 import qualified Liquid.GHC.API as GHC
 
 -- RJ: Please add docs
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
index 56ea4e1a2..4eeede09e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
@@ -159,7 +159,7 @@ pprXOT k (x, v) = (xd, pprintTidy k v)
   where
     xd          = maybe "unknown" (pprintTidy k) x
 
-instance PPrint LMap where
+instance (Ord v, F.Fixpoint v, PPrint v) => PPrint (LMapV v) where
   pprintTidy _ (LMap x xs e) = hcat [pprint x, pprint xs, text "|->", pprint e ]
 
 instance PPrint LogicMap where
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index 6007c3427..2e5e8564a 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -74,7 +74,7 @@ module Language.Haskell.Liquid.Types.Specs (
   ) where
 
 import           GHC.Generics            hiding (to, moduleName)
-import           Data.Bifunctor          (bimap, first)
+import           Data.Bifunctor          (bimap, first, second)
 import           Data.Bitraversable      (bimapM)
 import           Data.Binary
 import qualified Language.Fixpoint.Types as F
@@ -422,6 +422,7 @@ data Spec lname ty = Spec
   , dsize      :: ![([F.Located ty], lname)]                          -- ^ Size measure to enforce fancy termination
   , bounds     :: !(RRBEnvV lname (F.Located ty))
   , axeqs      :: ![F.EquationV lname]                                -- ^ Equalities used for Proof-By-Evaluation
+  , defines    :: ![(F.Located LHName, LMapV lname)]                  -- ^ Logic aliases
   } deriving (Data, Generic)
 
 instance (Show lname, F.PPrint lname, Show ty, F.PPrint ty, F.PPrint (RTypeV lname BTyCon BTyVar (RReftV lname))) => F.PPrint (Spec lname ty) where
@@ -488,6 +489,7 @@ emapSpecM bscp lenv vf f sp = do
         (traverse (emapBoundM (traverse . f) (\e -> emapExprVM (vf . (++ e)))))
         (M.toList $ bounds sp)
     axeqs <- mapM (emapEquationM vf) $ axeqs sp
+    defines <- mapM (traverse (emapLMapM vf)) $ defines sp
     return sp
       { measures
       , expSigs
@@ -511,6 +513,7 @@ emapSpecM bscp lenv vf f sp = do
       , dsize
       , bounds
       , axeqs
+      , defines
       }
   where
     fnull = f []
@@ -580,6 +583,7 @@ mapSpecLName f Spec {..} =
       , bounds = M.map (fmap (fmap f)) bounds
       , axeqs = map (fmap f) axeqs
       , dsize = map (fmap f) dsize
+      , defines = map (second $ fmap f) defines
       , ..
       }
   where
@@ -629,6 +633,7 @@ instance Semigroup (Spec lname ty) where
            , autosize   = S.union   (autosize s1)  (autosize s2)
            , bounds     = M.union   (bounds   s1)  (bounds   s2)
            , autois     = S.union   (autois s1)      (autois s2)
+           , defines    =            defines  s1 ++ defines  s2
            }
 
 instance Monoid (Spec lname ty) where
@@ -673,6 +678,7 @@ instance Monoid (Spec lname ty) where
            , dsize      = []
            , axeqs      = []
            , bounds     = M.empty
+           , defines    = []
            }
 
 -- $liftedSpec
@@ -754,6 +760,8 @@ data LiftedSpec = LiftedSpec
   , liftedBounds     :: RRBEnvV LHName LocBareTypeLHName
   , liftedAxeqs      :: HashSet (F.EquationV LHName)
     -- ^ Equalities used for Proof-By-Evaluation
+  , liftedDefines    :: HashMap F.Symbol (LMapV LHName)
+    -- ^ Logic aliases
   } deriving (Eq, Data, Generic)
     deriving Hashable via Generically LiftedSpec
     deriving Binary   via Generically LiftedSpec
@@ -805,6 +813,7 @@ emptyLiftedSpec = LiftedSpec
   , liftedDsize      = mempty
   , liftedBounds     = mempty
   , liftedAxeqs      = mempty
+  , liftedDefines    = mempty
   }
 
 -- $trackingDeps
@@ -979,6 +988,7 @@ toLiftedSpec a = LiftedSpec
   , liftedDsize      = dsize a
   , liftedBounds     = bounds a
   , liftedAxeqs      = S.fromList . axeqs $ a
+  , liftedDefines    = M.fromList . map (first (lhNameToResolvedSymbol . F.val)) . defines $ a
   }
 
 -- This is a temporary internal function that we use to convert the input dependencies into a format
@@ -1024,4 +1034,5 @@ unsafeFromLiftedSpec a = Spec
   , dsize      = liftedDsize  a
   , bounds     = liftedBounds a
   , axeqs      = S.toList . liftedAxeqs $ a
+  , defines    = map (first (dummyLoc . makeLocalLHName)) . M.toList . liftedDefines $ a
   }
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index 311631733..beb7762aa 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveDataTypeable         #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE DerivingVia                #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE FlexibleInstances          #-}
@@ -8,7 +9,6 @@
 {-# LANGUAGE UndecidableInstances       #-}
 {-# LANGUAGE OverloadedStrings          #-}
 {-# LANGUAGE ConstraintKinds            #-}
-{-# LANGUAGE DerivingVia                #-}
 {-# LANGUAGE NamedFieldPuns             #-}
 {-# LANGUAGE TupleSections              #-}
 
@@ -128,7 +128,7 @@ module Language.Haskell.Liquid.Types.Types (
   , mapRTAVars
 
   -- * CoreToLogic
-  , LogicMap(..), toLogicMap, eAppWithMap, LMap(..)
+  , LogicMap(..), toLMapV, mkLogicMap, toLogicMap, eAppWithMap, emapLMapM, LMapV(..), LMap
 
   -- * Refined Instances
   , RDEnv, DEnv(..), RInstance(..), RISig(..)
@@ -143,31 +143,33 @@ module Language.Haskell.Liquid.Types.Types (
   )
   where
 
-import           Liquid.GHC.API as Ghc hiding ( Expr
-                                                               , isFunTy
-                                                               , ($+$)
-                                                               , nest
-                                                               , text
-                                                               , blankLine
-                                                               , (<+>)
-                                                               , vcat
-                                                               , hsep
-                                                               , comma
-                                                               , colon
-                                                               , parens
-                                                               , empty
-                                                               , char
-                                                               , panic
-                                                               , int
-                                                               , hcat
-                                                               , showPpr
-                                                               , punctuate
-                                                               , ($$)
-                                                               , braces
-                                                               , angleBrackets
-                                                               , brackets
-                                                               )
+import           Liquid.GHC.API as Ghc hiding ( Binary
+                                              , Expr
+                                              , isFunTy
+                                              , ($+$)
+                                              , nest
+                                              , text
+                                              , blankLine
+                                              , (<+>)
+                                              , vcat
+                                              , hsep
+                                              , comma
+                                              , colon
+                                              , parens
+                                              , empty
+                                              , char
+                                              , panic
+                                              , int
+                                              , hcat
+                                              , showPpr
+                                              , punctuate
+                                              , ($$)
+                                              , braces
+                                              , angleBrackets
+                                              , brackets
+                                              )
 import           Data.String
+import           Data.Binary
 import           GHC.Generics
 import           Prelude                          hiding  (error)
 
@@ -261,19 +263,28 @@ instance Monoid LogicMap where
 instance Semigroup LogicMap where
   LM x1 x2 <> LM y1 y2 = LM (M.union x1 y1) (M.union x2 y2)
 
-data LMap = LMap
+data LMapV v = LMap
   { lmVar  :: F.LocSymbol
   , lmArgs :: [Symbol]
-  , lmExpr :: Expr
-  }
+  , lmExpr :: F.ExprV v
+  } deriving (Eq, Data, Generic, Functor)
+    deriving (Binary, Hashable) via Generically (LMapV v)
+type LMap = LMapV F.Symbol
 
-instance Show LMap where
+instance (Show v, Ord v, F.Fixpoint v) => Show (LMapV v) where
   show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
 
-toLogicMap :: [(F.LocSymbol, [Symbol], Expr)] -> LogicMap
-toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMap ls}
+toLMapV :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMapV v)
+toLMapV (x, (ys, e)) = (x, LMap {lmVar = getLHNameSymbol <$> x, lmArgs = ys, lmExpr = e})
+
+mkLogicMap :: M.HashMap Symbol LMap -> LogicMap
+mkLogicMap ls = mempty {lmSymDefs = ls}
+
+toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
+toLogicMap = mkLogicMap . M.fromList . map toLMapV0
   where
-    toLMap (x, ys, e) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
+  toLMapV0 :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
+  toLMapV0 (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
 
 eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
 eAppWithMap lmap f es expr
@@ -283,6 +294,11 @@ eAppWithMap lmap f es expr
   | otherwise
   = expr
 
+emapLMapM :: Monad m => ([Symbol] -> v0 -> m v1) -> LMapV v0 -> m (LMapV v1)
+emapLMapM f l = do
+    lmExpr <- emapExprVM (f . (++ lmArgs l)) (lmExpr l)
+    return l {lmExpr}
+
 --------------------------------------------------------------------------------
 -- | Refined Instances ---------------------------------------------------------
 --------------------------------------------------------------------------------
diff --git a/src/Data/Set_LHAssumptions.hs b/src/Data/Set_LHAssumptions.hs
index f95db559d..22e7dc97d 100644
--- a/src/Data/Set_LHAssumptions.hs
+++ b/src/Data/Set_LHAssumptions.hs
@@ -3,6 +3,7 @@
 module Data.Set_LHAssumptions where
 
 import Data.Set
+import Data.Set.Internal as I
 import GHC.Types_LHAssumptions()
 import Prelude hiding (null)
 
@@ -38,4 +39,24 @@ measure listElts :: [a] -> Set a
   listElts []     = {v | (Set_emp v)}
   listElts (x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }
 
+define singleton x      = (Set_sng x)
+define union x y        = (Set_cup x y)
+define intersection x y = (Set_cap x y)
+define difference x y   = (Set_dif x y)
+define empty            = (Set_empty 0)
+define null x           = (Set_emp x)
+define member x xs      = (Set_mem x xs)
+define isSubsetOf x y   = (Set_sub x y)
+define fromList xs      = (Data.Set_LHAssumptions.listElts xs)
+
+define I.singleton x      = (Set_sng x)
+define I.union x y        = (Set_cup x y)
+define I.intersection x y = (Set_cap x y)
+define I.difference x y   = (Set_dif x y)
+define I.empty            = (Set_empty 0)
+define I.null x           = (Set_emp x)
+define I.member x xs      = (Set_mem x xs)
+define I.isSubsetOf x y   = (Set_sub x y)
+define I.fromList xs      = (Data.Set_LHAssumptions.listElts xs)
+
 @-}
diff --git a/src/GHC/CString_LHAssumptions.hs b/src/GHC/CString_LHAssumptions.hs
index d41a028b9..0f7ef6f04 100644
--- a/src/GHC/CString_LHAssumptions.hs
+++ b/src/GHC/CString_LHAssumptions.hs
@@ -14,4 +14,6 @@ _f = unpackCString#
 assume GHC.CString.unpackCString#
   :: x:Addr#
   -> {v:[Char] | v ~~ x && len v == strLen x}
+
+define GHC.CString.unpackCString# x = x
 @-}
diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs
index 0e9e1389b..18a05479f 100644
--- a/src/GHC/Real_LHAssumptions.hs
+++ b/src/GHC/Real_LHAssumptions.hs
@@ -46,4 +46,9 @@ class (Real a, Enum a) => Integral a where
 
 //  fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here
 //  mod :: x:a -> y:a -> {v:a | v = (x mod y) }
+
+define div x y        = (x / y)
+define mod x y        = (x mod y)
+define fromIntegral x = (x)
+
 @-}
diff --git a/tests/benchmarks/popl18/ple/pos/Unification.hs b/tests/benchmarks/popl18/ple/pos/Unification.hs
index 7bad178a6..4a2ba626b 100644
--- a/tests/benchmarks/popl18/ple/pos/Unification.hs
+++ b/tests/benchmarks/popl18/ple/pos/Unification.hs
@@ -70,7 +70,7 @@ applyOne su (TFun tx t)
   = TFun (applyOne su tx) (applyOne su t)
 applyOne (P x t) (TVar v) | x == v
   = t
-applyOne _ t 
+applyOne _ t
   = t
 
 
@@ -105,17 +105,17 @@ split_fun :: Term -> Term -> Substitution -> Proof
       -> {apply θ (TFun t1 t2) == TFun (apply θ t1) (apply θ t2)} / [llen θ] @-}
 
 {-
-HACK: the above spe creates the rewrite rule 
+HACK: the above spe creates the rewrite rule
   apply θ (TFun t1 t2) -> TFun (apply θ t1) (apply θ t2)
-If I change the order of the equality to 
+If I change the order of the equality to
   TFun (apply θ t1) (apply θ t2) == apply θ (TFun t1 t2)
-then Liquid Haskell will not auto prove it  
+then Liquid Haskell will not auto prove it
 -}
 
 split_fun t1 t2 Emp
   = trivial
 split_fun t1 t2 (C su θ)
-   = split_fun t1 t2 θ --  &&& (applyOne su (TFun (apply θ t1) (apply θ t2)) *** QED) -- THIS 
+   = split_fun t1 t2 θ --  &&& (applyOne su (TFun (apply θ t1) (apply θ t2)) *** QED) -- THIS
 
 {-@ automatic-instances append_apply  @-}
 
@@ -135,8 +135,8 @@ append_apply (C su θ) θ2 t
 
 {-@ append_len ::  s1:Substitution -> s2:Substitution -> {llen (append s1 s2) == llen s1 + llen s2  } @-}
 append_len ::  Substitution -> Substitution -> Proof
-append_len Emp _       = trivial 
-append_len (C _ s1) s2 = append_len s1 s2 
+append_len Emp _       = trivial
+append_len (C _ s1) s2 = append_len s1 s2
 
 
 {-@ automatic-instances append_len  @-}
@@ -149,7 +149,7 @@ append_len (C _ s1) s2 = append_len s1 s2
              -> {apply (C (P i t) Emp) (TVar i) == apply (C (P i t) Emp) t } @-}
 theoremVar :: Term -> Int ->Proof
 theoremVar t i
-  =   theoremVarOne t i t 
+  =   theoremVarOne t i t
 
 
 {-@ automatic-instances theoremVarOne  @-}
@@ -160,9 +160,9 @@ theoremVar t i
              -> { applyOne (P i ti) t == t } @-}
 theoremVarOne :: Term -> Int -> Term -> Proof
 theoremVarOne (TFun t1 t2) i ti
-  = theoremVarOne t1 i ti &&& theoremVarOne t2 i ti 
+  = theoremVarOne t1 i ti &&& theoremVarOne t2 i ti
 theoremVarOne t i ti
-  = trivial 
+  = trivial
 
 
 
@@ -186,7 +186,7 @@ tsize (TFun t1 t2) = 1 + (tsize t1) + (tsize t2)
 {-@ reflect append @-}
 {-@ append :: xs:L a -> ys:L a -> {v:L a | llen v == llen xs + llen ys } @-}
 append :: L a -> L a -> L a
-append Emp ys = ys 
+append Emp ys = ys
 append (C x xs) ys = C x (append xs ys)
 
 data L a = Emp | C a (L a)
diff --git a/tests/neg/MyBag.hs b/tests/neg/MyBag.hs
new file mode 100644
index 000000000..9f7ae1b44
--- /dev/null
+++ b/tests/neg/MyBag.hs
@@ -0,0 +1,14 @@
+module MyBag where
+
+import qualified Data.Map as M
+
+{-@ embed Bag as Bag_t @-}
+data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
+
+{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+empty :: Bag k
+empty = Bag M.empty
+
+{-@ assume sng :: (Ord k) => k:k -> {v:Bag k | v = Bag_sng k 1} @-}
+sng :: (Ord k) => k -> Bag k
+sng k = Bag (M.singleton k 1)
diff --git a/tests/neg/MyBagDefine.hs b/tests/neg/MyBagDefine.hs
new file mode 100644
index 000000000..3b33b0448
--- /dev/null
+++ b/tests/neg/MyBagDefine.hs
@@ -0,0 +1,12 @@
+{-@ LIQUID "--expect-any-error" @-}
+module MyBagDefine where
+
+import MyBag
+import Data.Set
+
+{-@ define empty = (Bag_empty 0) @-}
+{-@ define sng k = (Bag_sng k 1) @-}
+
+{-@ thm_emp :: x:k -> { empty /= sng x } @-}
+thm_emp :: (Ord k) => k -> ()
+thm_emp x = const () (sng x)
diff --git a/tests/ple/pos/Isort_erase.hs b/tests/ple/pos/Isort_erase.hs
index 1e5c4eddf..c47eabfaa 100644
--- a/tests/ple/pos/Isort_erase.hs
+++ b/tests/ple/pos/Isort_erase.hs
@@ -1,7 +1,22 @@
 {-@ LIQUID "--reflection" @-}
 {-@ LIQUID "--ple"        @-}
 
-module Isort_erase where 
+{-
+This test relies on `withProof` being logically aliased to identity on the
+first argument, as `define`d in Language.Haskell.Liquid.ProofCombinators.
+Without this alias in scope, it will fail with the following error:
+
+    Liquid Type Mismatch
+
+    The inferred type
+      VV : {v : GHC.Types.Bool | Isort_erase.isSorted (Isort_erase.Cons y1 (Isort_erase.insert x ys))
+                                 && v == Isort_erase.lem_ins y1 x ys}
+
+    is not a subtype of the required type
+      VV : {VV : GHC.Types.Bool | Isort_erase.isSorted (Isort_erase.Cons y (Isort_erase.insert x ?a))}
+-}
+
+module Isort_erase where
 
 import Prelude hiding (id, sum)
 import Language.Haskell.Liquid.ProofCombinators
@@ -21,11 +36,11 @@ isSorted (Cons x xs) =
 
 {-@ reflect insert @-}
 {-@ insert :: x:Int -> {xs:List | isSorted xs} -> {xs:List | isSorted xs} @-}
-insert :: Int -> List -> List 
+insert :: Int -> List -> List
 insert x Emp     = Cons x Emp
 insert x (Cons y ys)
   | x <= y        = Cons x (Cons y ys)
-  | otherwise     = (Cons y (insert x ys)) `withProof` (lem_ins y x ys) 
+  | otherwise     = (Cons y (insert x ys)) `withProof` (lem_ins y x ys)
 
 {-@ lem_ins :: y:Int -> {x:Int | y < x} -> {ys:List | isSorted (Cons y ys)} -> {isSorted (Cons y (insert x ys))} @-}
 lem_ins :: Int -> Int -> List -> Bool
diff --git a/tests/pos/MyBag.hs b/tests/pos/MyBag.hs
new file mode 100644
index 000000000..9f7ae1b44
--- /dev/null
+++ b/tests/pos/MyBag.hs
@@ -0,0 +1,14 @@
+module MyBag where
+
+import qualified Data.Map as M
+
+{-@ embed Bag as Bag_t @-}
+data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
+
+{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+empty :: Bag k
+empty = Bag M.empty
+
+{-@ assume sng :: (Ord k) => k:k -> {v:Bag k | v = Bag_sng k 1} @-}
+sng :: (Ord k) => k -> Bag k
+sng k = Bag (M.singleton k 1)
diff --git a/tests/pos/MyBagDefine.hs b/tests/pos/MyBagDefine.hs
new file mode 100644
index 000000000..193b22e09
--- /dev/null
+++ b/tests/pos/MyBagDefine.hs
@@ -0,0 +1,12 @@
+module MyBagDefine where
+
+import MyBag as B
+import Data.Set
+
+{- dropping the qualification will trigger the "Ambiguous specification symbol" error -}
+{-@ define B.empty = (Bag_empty 0) @-}
+{-@ define sng k = (Bag_sng k 1) @-}
+
+{-@ thm_emp :: x:k -> { B.empty /= sng x } @-}
+thm_emp :: (Ord k) => k -> ()
+thm_emp x = const () (sng x)
diff --git a/tests/pos/NumRefl.hs b/tests/pos/NumRefl.hs
index 8ec0ace89..47425c1a8 100644
--- a/tests/pos/NumRefl.hs
+++ b/tests/pos/NumRefl.hs
@@ -1,10 +1,9 @@
 {-
 
-Without the 
-  define GHC.Internal.Num.fromInteger x = (x)
-  define GHC.Num.Integer.IS             = (x)
+Without the
+  define fromInteger x = (x)
 
-this program crashes with: 
+this program crashes with:
 
     Illegal type specification for `NumRefl.toNum`
     NumRefl.toNum :: forall p .
@@ -15,11 +14,13 @@ this program crashes with:
                                              && VV == (-GHC.Internal.Num.fromInteger (GHC.Num.Integer.IS 1))}
     The sort @(176) is not numeric
 
-Because the resule type (Num p) => p cannot be decided to be a numeric type.
+Because the result type (Num p) => p cannot be decided to be a numeric type.
 -}
 
 module NumRefl where
 
+{-@ define fromInteger x = (x) @-}
+
 {-@ reflect toNum @-}
 toNum :: Num p => () -> p
 toNum _ = -1
diff --git a/tests/pos/NumRefl1.hs b/tests/pos/NumRefl1.hs
new file mode 100644
index 000000000..bb9ba2068
--- /dev/null
+++ b/tests/pos/NumRefl1.hs
@@ -0,0 +1,12 @@
+module NumRefl1 where
+
+{-
+The `define` should be propagated from NumRefl, otherwise the test fails
+with the same error.
+-}
+import NumRefl
+
+{-@ reflect toNum1 @-}
+toNum1 :: Num p => () -> p
+toNum1 _ = -2
+
diff --git a/tests/tests.cabal b/tests/tests.cabal
index 9e15d4ada..c0a383853 100644
--- a/tests/tests.cabal
+++ b/tests/tests.cabal
@@ -1269,6 +1269,8 @@ executable unit-neg
                     , MultiParamTypeClasses
                     , MultipleInvariants
                     , Multi_pred_app_00
+                    , MyBag
+                    , MyBagDefine
                     , NameResolution
                     , NestedRecursion
                     , NoExhaustiveGuardsError
@@ -1862,7 +1864,10 @@ executable unit-pos-3
       buildable:      False
 
     other-modules:
-                      NumRefl
+                      MyBag
+                    , MyBagDefine
+                    , NumRefl
+                    , NumRefl1
                     , Streams
                     , StrictPair0
                     , StrictPair1