diff --git a/liquid-prelude.cabal b/liquid-prelude.cabal
--- a/liquid-prelude.cabal
+++ b/liquid-prelude.cabal
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-prelude
-version:            0.9.2.8.2
+version:            0.9.10.1.2
 synopsis:           General utility modules for LiquidHaskell
 description:        General utility modules for LiquidHaskell.
 license:            BSD3
@@ -30,5 +30,5 @@
                     , ghc-prim
                     , bytestring           >= 0.10.12.1
                     , containers           >= 0.6.4.1
-                    , liquidhaskell        >= 0.9.2.8
+                    , liquidhaskell        >= 0.9.10.1.2
   default-language:   Haskell2010
diff --git a/src/Language/Haskell/Liquid/Bag.hs b/src/Language/Haskell/Liquid/Bag.hs
--- a/src/Language/Haskell/Liquid/Bag.hs
+++ b/src/Language/Haskell/Liquid/Bag.hs
@@ -1,56 +1,71 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+
 module Language.Haskell.Liquid.Bag where
 
 import qualified Data.Map      as M
 
-{-@ embed   Data.Map.Map as Map_t                                         @-}
-
-{-@ measure Map_default :: Int -> Bag a                                   @-}
-{-@ measure Map_union   :: Bag a -> Bag a -> Bag a                        @-}
-{-@ measure Map_select  :: Data.Map.Map k v -> k -> v                     @-}
-{-@ measure Map_store   :: Data.Map.Map k v -> k -> v -> Data.Map.Map k v @-}
-{-@ measure bagSize     :: Bag k -> Int                                   @-}
+{-@ embed   Bag as Bag_t                             @-}
+{-@ measure bagSize       :: Bag a -> Int            @-}
 
 -- if I just write measure fromList the measure definition is not imported
 {-@ measure fromList :: [k] -> Bag k
-      fromList ([])   = (Map_default 0)
-      fromList (x:xs) = Map_store (fromList xs) x (1 + (Map_select (fromList xs) x))
+      fromList ([])   = (Bag_empty 0)
+      fromList (x:xs) = Bag_union (fromList xs) (Bag_sng x 1)
 @-}
 
 
-{-@ type Bag a = Data.Map.Map a Nat @-}
-type Bag a = M.Map a Int
+-- TODO newtype doesn't work because LH still expands the definition
+-- https://github.com/ucsd-progsys/liquidhaskell/issues/2332
+data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
 
-{-@ assume empty :: {v:Bag k | v = Map_default 0} @-}
+{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+{-@ define empty                = (Bag_empty 0) @-}
 empty :: Bag k
-empty = M.empty
-
-{-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}
-bagSize :: Bag k -> Int 
-bagSize b = sum (M.elems 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)
+empty = Bag M.empty
 
-{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Map_select b k}  @-}
+{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count k b}  @-}
+{-@ define get               k      b                    = (Bag_count k b) @-}
 get :: (Ord k) => k -> Bag k -> Int
-get k m = M.findWithDefault 0 k m
+get k b = M.findWithDefault 0 k (toMap b)
 
-{-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Map_store b k (1 + (Map_select b k))} @-}
-{-@ ignore put @-}
+{-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Bag_union b (Bag_sng k 1)} @-}
+{-@ define put               k      b                      = (Bag_union b (Bag_sng k 1)) @-}
 put :: (Ord k) => k -> Bag k -> Bag k
-put k m = M.insert k (1 + get k m) m
+put k b = Bag (M.insert k (1 + get k b) (toMap b))
 
-{-@ assume union :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Map_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 m1 m2 = M.union m1 m2
+union b1 b2 = Bag (M.unionWith (+) (toMap b1) (toMap b2))
 
-{-@ thm_emp :: x:k -> xs:Bag k ->  { Language.Haskell.Liquid.Bag.empty /= put x xs }  @-}
+{-@ 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) => 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) => 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 -> { empty /= put x xs } @-}
 thm_emp :: (Ord k) => k -> Bag k -> ()
 thm_emp x xs = const () (get x xs)
 
-{-@ assume thm_size :: xs:[k] ->  { bagSize (fromList xs) == len xs }  @-}
-thm_size :: (Ord k) => [k] -> ()  
-thm_size _ = () 
+{-@ assume thm_size :: xs:[k] -> { bagSize (fromList xs) == len xs } @-}
+thm_size :: (Ord k) => [k] -> ()
+thm_size _ = ()
diff --git a/src/Language/Haskell/Liquid/Foreign.hs b/src/Language/Haskell/Liquid/Foreign.hs
--- a/src/Language/Haskell/Liquid/Foreign.hs
+++ b/src/Language/Haskell/Liquid/Foreign.hs
@@ -35,7 +35,7 @@
 cSizeInt = fromIntegral
 
 
-{-@ assume mkPtr :: x:GHC.Prim.Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}
+{-@ assume mkPtr :: x:Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}
 mkPtr   :: Addr# -> Ptr b
 mkPtr = undefined -- Ptr x
 
diff --git a/src/Language/Haskell/Liquid/Prelude.hs b/src/Language/Haskell/Liquid/Prelude.hs
--- a/src/Language/Haskell/Liquid/Prelude.hs
+++ b/src/Language/Haskell/Liquid/Prelude.hs
@@ -134,10 +134,18 @@
 safeZipWith _ []     []     = []
 safeZipWith _ _ _ = error "safeZipWith: cannot happen!"
 
-{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p =>  q)} @-}
+{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p => q)} @-}
 infixr 8 ==>
 (==>) :: Bool -> Bool -> Bool
 False ==> False = True
 False ==> True  = True
 True  ==> True  = True
 True  ==> False = False
+
+{-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p <=> q)} @-}
+infixr 8 <=>
+(<=>) :: Bool -> Bool -> Bool
+False <=> False = True
+False <=> True  = False
+True  <=> True  = True
+True  <=> False = False
diff --git a/src/Language/Haskell/Liquid/ProofCombinators.hs b/src/Language/Haskell/Liquid/ProofCombinators.hs
--- a/src/Language/Haskell/Liquid/ProofCombinators.hs
+++ b/src/Language/Haskell/Liquid/ProofCombinators.hs
@@ -10,7 +10,7 @@
 
   -- * Proof is just a () alias
   Proof
-  , toProof 
+  , toProof
 
   -- * Proof constructors
   , trivial, unreachable, (***), QED(..)
@@ -21,18 +21,18 @@
   -- * 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
@@ -75,8 +75,10 @@
 
 data QED = Admit | QED
 
-{-@ measure isAdmit :: QED -> Bool @-}
-{-@ Admit :: {v:QED | isAdmit v } @-}
+{-@ measure isAdmit @-}
+isAdmit :: QED -> Bool
+isAdmit Admit = True
+isAdmit QED   = False
 
 
 -------------------------------------------------------------------------------
@@ -120,9 +122,9 @@
 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 +151,13 @@
 -- | 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 +167,8 @@
 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 +177,7 @@
 impossible _ = undefined
 
 -------------------------------------------------------------------------------
--- | Convenient Syntax for Inductive Propositions 
+-- | Convenient Syntax for Inductive Propositions
 -------------------------------------------------------------------------------
 
 {-@ measure prop :: a -> b           @-}