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.12.2.1
+version:            0.9.14.1
 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.12.2.1
+                    , liquidhaskell        >= 0.9.14.1
   default-language:   Haskell2010
diff --git a/src/Language/Haskell/Liquid/Equational.hs b/src/Language/Haskell/Liquid/Equational.hs
--- a/src/Language/Haskell/Liquid/Equational.hs
+++ b/src/Language/Haskell/Liquid/Equational.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
-module Language.Haskell.Liquid.Equational where 
+module Language.Haskell.Liquid.Equational where
 
 -------------------------------------------------------------------------------
 -- | Proof is just unit
@@ -8,34 +8,34 @@
 type Proof = ()
 
 -------------------------------------------------------------------------------
--- | Casting expressions to Proof using the "postfix" `*** QED` 
+-- | Casting expressions to Proof using the "postfix" `*** QED`
 -------------------------------------------------------------------------------
 
-data QED = QED 
+data QED = QED
 
 infixl 2 ***
 (***) :: a -> QED -> Proof
-_ *** QED = () 
+_ *** QED = ()
 
 -------------------------------------------------------------------------------
--- | Equational Reasoning operators 
--- | The `eq` operator is inlined in the logic, so can be used in reflected 
--- | functions while ignoring the equality steps. 
+-- | Equational Reasoning operators
+-- | The `eq` operator is inlined in the logic, so can be used in reflected
+-- | functions while ignoring the equality steps.
 -------------------------------------------------------------------------------
 
-infixl 3 ==., `eq` 
+infixl 3 ==., `eq`
 
 
 {-@ (==.) :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}
-(==.) :: a -> a -> a 
-_ ==. x = x 
-{-# INLINE (==.) #-} 
+(==.) :: a -> a -> a
+_ ==. x = x
+{-# INLINE (==.) #-}
 
 
 {-@ eq :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}
-eq :: a -> a -> a 
-_ `eq` x = x 
-{-# INLINE eq #-} 
+eq :: a -> a -> a
+_ `eq` x = x
+{-# INLINE eq #-}
 
 -------------------------------------------------------------------------------
 -- | Explanations
@@ -44,13 +44,13 @@
 infixl 3 ?
 
 {-@ (?) :: forall a b <pa :: a -> Bool>. a<pa> -> b -> a<pa> @-}
-(?) :: a -> b -> a 
-x ? _ = x 
-{-# INLINE (?)   #-} 
+(?) :: a -> b -> a
+x ? _ = x
+{-# INLINE (?)   #-}
 
 -------------------------------------------------------------------------------
--- | Using proofs as theorems 
+-- | Using proofs as theorems
 -------------------------------------------------------------------------------
 
-withTheorem :: a -> Proof -> a 
-withTheorem z _ = z 
+withTheorem :: a -> Proof -> a
+withTheorem z _ = z
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
@@ -127,7 +127,7 @@
 
 -----------------------------------------------------------------------------------------------
 
-{-@ safeZipWith :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len v = len xs} 
+{-@ safeZipWith :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len v = len xs}
                 -> {v : [c] | len v = len xs } @-}
 safeZipWith :: (a->b->c) -> [a]->[b]->[c]
 safeZipWith f (a:as) (b:bs) = f a b : safeZipWith f as bs
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
@@ -115,20 +115,44 @@
 _ =>= y  = y
 
 -------------------------------------------------------------------------------
--- | `?` is basically Haskell's $ and is used for the right precedence
--- | `?` lets you "add" some fact into a proof term
+-- | @e ? lemma@ lets you use the type of @lemma@ when checking that @e@ haskell
+-- has some expected refinement type.
+--
+-- Schematically, @?@ allows to use @q x@ to check that @e@ satisfies @p x e@
+-- in the following function.
+--
+-- > f :: x:t0 -> {v:t1 | p x v}
+-- > f x = e ? lemma x
+-- >   where
+-- >     lemma :: y:t0 -> { q y }
+-- >     lemma = ...
+--
+-- While @?@ is defined as Haskell's 'const', @?@ is optimized by Liquid
+-- Haskell. The 'const' function, on the other hand, would incur some extra
+-- verification overhead because Liquid Haskell needs to go through the trouble
+-- of checking that @const e lemma@ is actually @e@.
+--
+-- === At a lower level
+--
+-- Liquid Haskell treats @e ? lemma@ as
+--
+-- > let fresh0 = e
+-- >  in let fresh1 = lemma
+-- >      in fresh0
+--
+-- Which makes the @fresh1@ binding available in the environment of whatever
+-- constraints arise in the inner occurrence of @fresh0@.
 -------------------------------------------------------------------------------
 
 infixl 3 ?
 
-{-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
 (?) :: a -> b -> a
 x ? _ = x
 {-# INLINE (?)   #-}
 
 -------------------------------------------------------------------------------
 -- | Assumed equality
--- 	`x ==! y `
+--      `x ==! y `
 --   returns the admitted proof certificate that result value is equals x and y
 -------------------------------------------------------------------------------
 
@@ -140,9 +164,9 @@
 
 -- | To summarize:
 --
--- 	- (==!) is *only* for proof debugging
---	- (===) does not require explicit proof term
--- 	- (?)   lets you insert "lemmas" as other `Proof` values
+--      - (==!) is *only* for proof debugging
+--      - (===) does not require explicit proof term
+--      - (?)   lets you insert "lemmas" as other `Proof` values
 
 -------------------------------------------------------------------------------
 -- | * Unchecked Proof Certificates -------------------------------------------
diff --git a/src/Language/Haskell/Liquid/String.hs b/src/Language/Haskell/Liquid/String.hs
--- a/src/Language/Haskell/Liquid/String.hs
+++ b/src/Language/Haskell/Liquid/String.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
--- Support for Strings for SMT 
+-- Support for Strings for SMT
 
 {-# LANGUAGE OverloadedStrings   #-}
 
@@ -10,7 +10,7 @@
 
 {-@ embed SMTString as Str @-}
 
-data SMTString = S BS.ByteString 
+data SMTString = S BS.ByteString
   deriving (Eq, Show)
 
 {-@ invariant {s:SMTString | 0 <= stringLen s } @-}
@@ -25,7 +25,7 @@
 
 ----------------------------------
 
-{-@ assume concatString :: x:SMTString -> y:SMTString 
+{-@ assume concatString :: x:SMTString -> y:SMTString
                  -> {v:SMTString | v == concatString x y && stringLen v == stringLen x + stringLen y } @-}
 concatString :: SMTString -> SMTString -> SMTString
 concatString (S s1) (S s2) = S (s1 `BS.append` s2)
@@ -34,30 +34,30 @@
 stringEmp :: SMTString
 stringEmp = S (BS.empty)
 
-stringLen :: SMTString -> Int  
+stringLen :: SMTString -> Int
 {-@ assume stringLen :: x:SMTString -> {v:Nat | v == stringLen x} @-}
-stringLen (S s) = BS.length s 
+stringLen (S s) = BS.length s
 
 
 {-@ assume subString  :: s:SMTString -> offset:Int -> ln:Int -> {v:SMTString | v == subString s offset ln } @-}
-subString :: SMTString -> Int -> Int -> SMTString 
-subString (S s) o l = S (BS.take l $ BS.drop o s) 
+subString :: SMTString -> Int -> Int -> SMTString
+subString (S s) o l = S (BS.take l $ BS.drop o s)
 
 
-{-@ assume takeString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == i && v == takeString i xs } @-} 
+{-@ assume takeString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == i && v == takeString i xs } @-}
 takeString :: Int -> SMTString -> SMTString
 takeString i (S s) = S (BS.take i s)
 
-{-@ assume dropString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == stringLen xs - i && v == dropString i xs } @-} 
+{-@ assume dropString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == stringLen xs - i && v == dropString i xs } @-}
 dropString :: Int -> SMTString -> SMTString
 dropString i (S s) = S (BS.drop i s)
 
 
 {-@ assume fromString :: i:String -> {o:SMTString | i == o && o == fromString i} @-}
 fromString :: String -> SMTString
-fromString = S . ST.fromString 
+fromString = S . ST.fromString
 
 
-{-@ assume isNullString :: i:SMTString -> {b:Bool | b <=> stringLen i == 0 } @-} 
-isNullString :: SMTString -> Bool 
-isNullString (S s) = BS.length s == 0 
+{-@ assume isNullString :: i:SMTString -> {b:Bool | b <=> stringLen i == 0 } @-}
+isNullString :: SMTString -> Bool
+isNullString (S s) = BS.length s == 0