diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,12 @@
 * Hackage: <http://hackage.haskell.org/package/sbv>
 * GitHub:  <http://github.com/LeventErkok/sbv>
 
+### Version 11.3, 2025-03-10
+
+  * Fix various haddock documentation links
+
+  * KD: Clean-up proofs using the cases tactic
+
 ### Version 11.2, 2025-03-08
 
   * Renamed the all-sat partitioning function from 'partition' to 'allSatPartiton'
diff --git a/Data/SBV.hs b/Data/SBV.hs
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -24,8 +24,8 @@
 -- And similarly, 'sat' finds a satisfying instance. The types involved are:
 --
 -- @
---     'prove' :: 'Provable' a => a -> 'IO' 'ThmResult'
---     'sat'   :: 'Data.SBV.Provers.Satisfiable' a => a -> 'IO' 'SatResult'
+--     'prove' :: 'Provable' a => a -> 'IO' t'ThmResult'
+--     'sat'   :: 'Data.SBV.Provers.Satisfiable' a => a -> 'IO' t'SatResult'
 -- @
 --
 -- The classes 'Provable' and 'Data.SBV.Provers.Satisfiable' come with instances for n-ary predicates, for arbitrary n.
@@ -385,7 +385,7 @@
   -- $softAssertions
   , assertWithPenalty , Penalty(..)
   -- ** Field extensions
-  -- | If an optimization results in an infinity/epsilon value, the returned `CV` value will be in the corresponding extension field.
+  -- | If an optimization results in an infinity/epsilon value, the returned t'CV' value will be in the corresponding extension field.
   , ExtCV(..), GeneralizedCV(..)
 
   -- * Model extraction
@@ -425,7 +425,7 @@
   , some
 
   -- * Queriable values
-  , Queriable(..), freshVar, freshVar_, getValue
+  , Queriable(..), freshVar, freshVar_
 
   -- * Module exports
   -- $moduleExportIntro
@@ -727,8 +727,8 @@
 
        @
          'assertWithPenalty' "bounded_x" (x .< 5) 'DefaultPenalty'
-         'assertWithPenalty' "bounded_x" (x .< 5) ('Penalty' 2.3 Nothing)
-         'assertWithPenalty' "bounded_x" (x .< 5) ('Penalty' 4.7 (Just "group-1")) @
+         'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 2.3 Nothing
+         'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 4.7 (Just "group-1") @
 
   In the first form, we are saying that the constraint @x .< 5@ must be satisfied, if possible,
   but if this constraint can not be satisfied to find a model, it can be violated with the default penalty of 1.
@@ -749,7 +749,7 @@
 -}
 
 {- $resultTypes
-'ThmResult', 'SatResult', and 'AllSatResult' are simple newtype wrappers over 'SMTResult'. Their
+t'ThmResult', t'SatResult', and t'AllSatResult' are simple newtype wrappers over t'SMTResult'. Their
 main purpose is so that we can provide custom 'Show' instances to print results accordingly.
 -}
 
@@ -993,8 +993,8 @@
    * "Documentation.SBV.Examples.Puzzles.Rabbits"
    * "Documentation.SBV.Examples.Misc.FirstOrderLogic"
 
-SBV also supports the constructors 'ExistsUnique' to create unique existentials, in addition to
-'ForallN' and 'ExistsN' for creating multiple variables at the same time.
+SBV also supports the constructors t'ExistsUnique' to create unique existentials, in addition
+to t'ForallN' and t'ExistsN' for creating multiple variables at the same time.
 
 In general, SBV will not display the values of quantified variables for a satisfying instance.
 For a satisfiability problem, you can apply skolemization manually to have these values
@@ -1168,7 +1168,7 @@
 
 {- $verbosity
 
-SBV provides various levels of verbosity to aid in debugging, by using the 'SMTConfig' fields:
+SBV provides various levels of verbosity to aid in debugging, by using the t'SMTConfig' fields:
 
   * ['verbose'] Print on stdout a shortened account of what is sent/received. This is specifically trimmed to reduce noise
     and is good for quick debugging. The output is not supposed to be machine-readable.
@@ -1774,7 +1774,7 @@
   project :: a -> QueryT m (QueryResult a)
 
   -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
-  -- via the 'QueryT' monad transformer.
+  -- via the t'QueryT' monad transformer.
   embed   :: QueryResult a -> QueryT m a
 
   default project :: (a ~ t e, QueryResult (t e) ~ t (QueryResult e), Traversable t, Monad m, Queriable m e) =>  a -> QueryT m (QueryResult a)
diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs
--- a/Data/SBV/Compilers/C.hs
+++ b/Data/SBV/Compilers/C.hs
@@ -62,7 +62,7 @@
                                renderCgPgmBundle mbDirName (cfg, bundle)
                                return retVal
 
--- | Lower level version of 'compileToC', producing a 'CgPgmBundle'
+-- | Lower level version of 'compileToC', producing a t'CgPgmBundle'
 compileToC' :: String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
 compileToC' nm f = do rands <- randoms `fmap` newStdGen
                       codeGen SBVToC (defaultCgConfig { cgDriverVals = rands }) nm f
@@ -82,7 +82,7 @@
                                            renderCgPgmBundle mbDirName (cfg, pgm)
                                            return retVal
 
--- | Lower level version of 'compileToCLib', producing a 'CgPgmBundle'
+-- | Lower level version of 'compileToCLib', producing a t'CgPgmBundle'
 compileToCLib' :: String -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
 compileToCLib' libName comps = do resCfgBundles <- mapM (uncurry compileToC') comps
                                   let (finalCfg, finalPgm) = mergeToLib libName [(c, b) | (_, c, b) <- resCfgBundles]
diff --git a/Data/SBV/Control.hs b/Data/SBV/Control.hs
--- a/Data/SBV/Control.hs
+++ b/Data/SBV/Control.hs
@@ -27,6 +27,9 @@
      -- ** Extracting the unsat core
      , getUnsatCore
 
+     -- ** Getting the model value for a symbolic variable
+     , getValue
+
      -- ** Extracting a proof
      , getProof
 
diff --git a/Data/SBV/Control/BaseIO.hs b/Data/SBV/Control/BaseIO.hs
--- a/Data/SBV/Control/BaseIO.hs
+++ b/Data/SBV/Control/BaseIO.hs
@@ -192,7 +192,7 @@
 -- @
 --
 -- for this call to not error out! Furthermore, unsat-cores require for the user to name the
--- constraints to be considered as part of the set, which is done via 'Data.SBV.Core.namedConstraint'.
+-- constraints to be considered as part of the set, which is done via 'Data.SBV.namedConstraint'.
 --
 -- NB. There is no notion of a minimal unsat-core, in case unsatisfiability can be derived
 -- in multiple ways. Furthermore, Z3 does not guarantee that the generated unsat
diff --git a/Data/SBV/Core/Concrete.hs b/Data/SBV/Core/Concrete.hs
--- a/Data/SBV/Core/Concrete.hs
+++ b/Data/SBV/Core/Concrete.hs
@@ -192,7 +192,7 @@
                                                                  ]
                                             else cvRank a `compare` cvRank b
 
--- | 'CV' represents a concrete word of a fixed size:
+-- | A t'CV' represents a concrete word of a fixed size:
 -- For signed words, the most significant digit is considered to be the sign.
 data CV = CV { _cvKind  :: !Kind
              , cvVal    :: !CVal
@@ -300,15 +300,15 @@
 normCV c                         = c
 {-# INLINE normCV #-}
 
--- | Constant False as a 'CV'. We represent it using the integer value 0.
+-- | Constant False as a t'CV'. We represent it using the integer value 0.
 falseCV :: CV
 falseCV = CV KBool (CInteger 0)
 
--- | Constant True as a 'CV'. We represent it using the integer value 1.
+-- | Constant True as a t'CV'. We represent it using the integer value 1.
 trueCV :: CV
 trueCV  = CV KBool (CInteger 1)
 
--- | Map a unary function through a 'CV'.
+-- | Map a unary function through a t'CV'.
 mapCV :: (AlgReal             -> AlgReal)
       -> (Integer             -> Integer)
       -> (Float               -> Float)
@@ -333,7 +333,7 @@
                                                     CEither{}   -> error "Data.SBV.mapCV: Unexpected call through mapCV with either!"
                                                     CArray{}    -> error "Data.SBV.mapCV: Unexpected call through mapCV with arrays!"
 
--- | Map a binary function through a 'CV'.
+-- | Map a binary function through a t'CV'.
 mapCV2 :: (AlgReal             -> AlgReal             -> AlgReal)
        -> (Integer             -> Integer             -> Integer)
        -> (Float               -> Float               -> Float)
@@ -361,11 +361,11 @@
                                         , "*** Please report this as a bug!"
                                         ]
 
--- | Show instance for 'CV'.
+-- | Show instance for t'CV'.
 instance Show CV where
   show = showCV True
 
--- | Show instance for Generalized 'CV'
+-- | Show instance for Generalized t'CV'
 instance Show GeneralizedCV where
   show (ExtendedCV k) = showExtCV True k
   show (RegularCV  c) = showCV    True c
@@ -515,7 +515,7 @@
     bounds False w = (0, 2^w - 1)
     bounds True  w = (-x, x-1) where x = 2^(w-1)
 
--- | Generate a random constant value ('CV') of the correct kind.
+-- | Generate a random constant value (i.e., t'CV') of the correct kind.
 randomCV :: Kind -> IO CV
 randomCV k = CV k <$> randomCVal k
 
diff --git a/Data/SBV/Core/Sized.hs b/Data/SBV/Core/Sized.hs
--- a/Data/SBV/Core/Sized.hs
+++ b/Data/SBV/Core/Sized.hs
@@ -42,22 +42,22 @@
 -- | An unsigned bit-vector carrying its size info
 newtype WordN (n :: Nat) = WordN Integer deriving (Eq, Ord)
 
--- | Show instance for 'WordN'
+-- | Show instance for t'WordN'
 instance Show (WordN n) where
   show (WordN v) = show v
 
--- | 'WordN' has a kind
+-- | t'WordN' has a kind
 instance (KnownNat n, BVIsNonZero n) => HasKind (WordN n) where
   kindOf _ = KBounded False (intOfProxy (Proxy @n))
 
 -- | A signed bit-vector carrying its size info
 newtype IntN (n :: Nat) = IntN Integer deriving (Eq, Ord)
 
--- | Show instance for 'IntN'
+-- | Show instance for t'IntN'
 instance Show (IntN n) where
   show (IntN v) = show v
 
--- | 'IntN' has a kind
+-- | t'IntN' has a kind
 instance (KnownNat n, BVIsNonZero n) => HasKind (IntN n) where
   kindOf _ = KBounded True (intOfProxy (Proxy @n))
 
@@ -93,17 +93,17 @@
         uc (SVal _ (Left v)) = cvToBool v
         uc r                 = error $ "Impossible happened while lifting " ++ show nm ++ " over " ++ show (k, x, i, r)
 
--- | 'Bounded' instance for 'WordN'
+-- | 'Bounded' instance for t'WordN'
 instance (KnownNat n, BVIsNonZero n) => Bounded (WordN n) where
    minBound = WordN 0
    maxBound = let sz = intOfProxy (Proxy @n) in WordN $ 2 ^ sz - 1
 
--- | 'Bounded' instance for 'IntN'
+-- | 'Bounded' instance for t'IntN'
 instance (KnownNat n, BVIsNonZero n) => Bounded (IntN n) where
    minBound = let sz1 = intOfProxy (Proxy @n) - 1 in IntN $ - (2 ^ sz1)
    maxBound = let sz1 = intOfProxy (Proxy @n) - 1 in IntN $ 2 ^ sz1 - 1
 
--- | 'Num' instance for 'WordN'
+-- | 'Num' instance for t'WordN'
 instance (KnownNat n, BVIsNonZero n) => Num (WordN n) where
    (+)         = lift2 "(+)"    svPlus
    (-)         = lift2 "(*)"    svMinus
@@ -113,7 +113,7 @@
    signum      = WordN . signum   . toInteger
    fromInteger = WordN . fromJust . svAsInteger . svInteger (kindOf (undefined :: WordN n))
 
--- | 'Num' instance for 'IntN'
+-- | 'Num' instance for t'IntN'
 instance (KnownNat n, BVIsNonZero n) => Num (IntN n) where
    (+)         = lift2 "(+)"    svPlus
    (-)         = lift2 "(*)"    svMinus
@@ -123,35 +123,35 @@
    signum      = IntN . signum   . toInteger
    fromInteger = IntN . fromJust . svAsInteger . svInteger (kindOf (undefined :: IntN n))
 
--- | 'Enum' instance for 'WordN'
+-- | 'Enum' instance for t'WordN'
 instance (KnownNat n, BVIsNonZero n) => Enum (WordN n) where
    toEnum   = fromInteger  . toInteger
    fromEnum = fromIntegral . toInteger
 
--- | 'Enum' instance for 'IntN'
+-- | 'Enum' instance for t'IntN'
 instance (KnownNat n, BVIsNonZero n) => Enum (IntN n) where
    toEnum   = fromInteger  . toInteger
    fromEnum = fromIntegral . toInteger
 
--- | 'Real' instance for 'WordN'
+-- | 'Real' instance for t'WordN'
 instance (KnownNat n, BVIsNonZero n) => Real (WordN n) where
    toRational (WordN x) = toRational x
 
--- | 'Real' instance for 'IntN'
+-- | 'Real' instance for t'IntN'
 instance (KnownNat n, BVIsNonZero n) => Real (IntN n) where
    toRational (IntN x) = toRational x
 
--- | 'Integral' instance for 'WordN'
+-- | 'Integral' instance for t'WordN'
 instance (KnownNat n, BVIsNonZero n) => Integral (WordN n) where
    toInteger (WordN x)           = x
    quotRem   (WordN x) (WordN y) = let (q, r) = quotRem x y in (WordN q, WordN r)
 
--- | 'Integral' instance for 'IntN'
+-- | 'Integral' instance for t'IntN'
 instance (KnownNat n, BVIsNonZero n) => Integral (IntN n) where
    toInteger (IntN x)          = x
    quotRem   (IntN x) (IntN y) = let (q, r) = quotRem x y in (IntN q, IntN r)
 
---  'Bits' instance for 'WordN'
+--  'Bits' instance for t'WordN'
 instance (KnownNat n, BVIsNonZero n) => Bits (WordN n) where
    (.&.)        = lift2   "(.&.)"      svAnd
    (.|.)        = lift2   "(.|.)"      svOr
@@ -168,7 +168,7 @@
    bit i        = 1 `shiftL` i
    popCount     = fromIntegral . popCount . toInteger
 
---  'Bits' instance for 'IntN'
+--  'Bits' instance for t'IntN'
 instance (KnownNat n, BVIsNonZero n) => Bits (IntN n) where
    (.&.)        = lift2   "(.&.)"      svAnd
    (.|.)        = lift2   "(.|.)"      svOr
diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs
--- a/Data/SBV/Core/Symbolic.hs
+++ b/Data/SBV/Core/Symbolic.hs
@@ -195,11 +195,11 @@
 forceSVArg :: SV -> IO ()
 forceSVArg (SV k n) = k `seq` n `seq` return ()
 
--- | Constant False as an 'SV'. Note that this value always occupies slot -2 and level 0.
+-- | Constant False as an t'SV'. Note that this value always occupies slot -2 and level 0.
 falseSV :: SV
 falseSV = SV KBool $ NodeId (globalSBVContext, Just 0, -2)
 
--- | Constant True as an 'SV'. Note that this value always occupies slot -1 and level 0.
+-- | Constant True as an t'SV'. Note that this value always occupies slot -1 and level 0.
 trueSV :: SV
 trueSV  = SV KBool $ NodeId (globalSBVContext, Just 0, -1)
 
@@ -752,7 +752,7 @@
 -- | Helper synonym for text, in case we switch to something else later.
 type Name = T.Text
 
--- | 'NamedSymVar' pairs symbolic values and user given/automatically generated names
+-- | t'NamedSymVar' pairs symbolic values and user given/automatically generated names
 data NamedSymVar = NamedSymVar !SV !Name
                  deriving (Show, Generic, G.Data)
 
@@ -799,7 +799,7 @@
 
 -- | Penalty for a soft-assertion. The default penalty is @1@, with all soft-assertions belonging
 -- to the same objective goal. A positive weight and an optional group can be provided by using
--- the 'Penalty' constructor.
+-- the v'Penalty' constructor.
 data Penalty = DefaultPenalty                  -- ^ Default: Penalty of @1@ and no group attached
              | Penalty Rational (Maybe String) -- ^ Penalty with a weight and an optional group
              deriving Show
@@ -1285,7 +1285,7 @@
 instance HasKind SVal where
   kindOf (SVal k _) = k
 
--- Show instance for 'SVal'. Not particularly "desirable", but will do if needed
+-- Show instance for t'SVal'. Not particularly "desirable", but will do if needed
 -- NB. We do not show the type info on constant KBool values, since there's no
 -- implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement
 -- of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!)
@@ -1296,7 +1296,7 @@
 
 -- | This instance is only defined so that we can define an instance for
 -- 'Data.Bits.Bits'. '==' and '/=' simply throw an error.
--- We really don't want an 'Eq' instance for 'Data.SBV.Core.SBV' or 'SVal'. As it really makes no sense.
+-- We really don't want an 'Eq' instance for 'Data.SBV.SBV' or t'SVal'. As it really makes no sense.
 -- But since we do want the 'Data.Bits.Bits' instance, we're forced to define equality. See
 -- <http://github.com/LeventErkok/sbv/issues/301>. We simply error out.
 instance Eq SVal where
@@ -1706,7 +1706,7 @@
   ask = lift ask
   local f = mapSymbolicT $ mapReaderT $ local f
 
--- | 'Symbolic' is specialization of 'SymbolicT' to the `IO` monad. Unless you are using
+-- | 'Symbolic' is specialization of t'SymbolicT' to the `IO` monad. Unless you are using
 -- transformers explicitly, this is the type you should prefer.
 type Symbolic = SymbolicT IO
 
@@ -2355,7 +2355,7 @@
 isEmptyModel SMTModel{modelAssocs, modelUIFuns} = null modelAssocs && null modelUIFuns
 
 -- | The result of an SMT solver call. Each constructor is tagged with
--- the 'SMTConfig' that created it so that further tools can inspect it
+-- the t'SMTConfig' that created it so that further tools can inspect it
 -- and build layers of results, if needed. For ordinary uses of the library,
 -- this type should not be needed, instead use the accessor functions on
 -- it. (Custom Show instances and model extractors.)
diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs
--- a/Data/SBV/Dynamic.hs
+++ b/Data/SBV/Dynamic.hs
@@ -201,14 +201,14 @@
 
 -- | Prove a property with query mode using multiple threads. Each query
 -- computation will spawn a thread and a unique instance of your solver to run
--- asynchronously. The 'Symbolic' 'SVal' is duplicated for each thread. This
+-- asynchronously. The 'Symbolic' t'SVal' is duplicated for each thread. This
 -- function will block until all child threads return.
 proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)]
 proveConcurrentWithAll cfg s queries = SBV.proveConcurrentWithAll cfg queries (fmap toSBool s)
 
 -- | Prove a property with query mode using multiple threads. Each query
 -- computation will spawn a thread and a unique instance of your solver to run
--- asynchronously. The 'Symbolic' 'SVal' is duplicated for each thread. This
+-- asynchronously. The 'Symbolic' t'SVal' is duplicated for each thread. This
 -- function will return the first query computation that completes, killing the others.
 proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult)
 proveConcurrentWithAny cfg s queries = SBV.proveConcurrentWithAny cfg queries (fmap toSBool s)
@@ -226,14 +226,14 @@
 satWithAny cfgs s = SBV.satWithAny cfgs (fmap toSBool s)
 
 -- | Find a satisfying assignment to a property with multiple threads in query
--- mode. The 'Symbolic' 'SVal' represents what is known to all child query threads.
+-- mode. The 'Symbolic' t'SVal' represents what is known to all child query threads.
 -- Each query thread will spawn a unique instance of the solver. Only the first
 -- one to finish will be returned and the other threads will be killed.
 satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
 satConcurrentWithAny cfg qs s = SBV.satConcurrentWithAny cfg qs (fmap toSBool s)
 
 -- | Find a satisfying assignment to a property with multiple threads in query
--- mode. The 'Symbolic' 'SVal' represents what is known to all child query threads.
+-- mode. The 'Symbolic' t'SVal' represents what is known to all child query threads.
 -- Each query thread will spawn a unique instance of the solver. This function
 -- will block until all child threads have completed.
 satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs
--- a/Data/SBV/Provers/Prover.hs
+++ b/Data/SBV/Provers/Prover.hs
@@ -774,7 +774,7 @@
   where comp =  do _ <- reducer a >>= output
                    Control.executeQuery QueryInternal q
 
--- | Check if a safe-call was safe or not, turning a 'SafeResult' to a Bool.
+-- | Check if a safe-call was safe or not, turning a t'SafeResult' to a Bool.
 isSafe :: SafeResult -> Bool
 isSafe (SafeResult (_, _, result)) = case result of
                                        Unsatisfiable{} -> True
diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs
--- a/Data/SBV/SMT/SMT.hs
+++ b/Data/SBV/SMT/SMT.hs
@@ -101,24 +101,24 @@
 resultConfig (Unknown       c _  ) = c
 resultConfig (ProofError    c _ _) = c
 
--- | A 'Data.SBV.prove' call results in a 'ThmResult'
+-- | A 'Data.SBV.prove' call results in a t'ThmResult'
 newtype ThmResult = ThmResult SMTResult
                   deriving NFData
 
--- | A 'Data.SBV.sat' call results in a 'SatResult'
--- The reason for having a separate 'SatResult' is to have a more meaningful 'Show' instance.
+-- | A 'Data.SBV.sat' call results in a t'SatResult'
+-- The reason for having a separate t'SatResult' is to have a more meaningful 'Show' instance.
 newtype SatResult = SatResult SMTResult
                   deriving NFData
 
--- | An 'Data.SBV.allSat' call results in a 'AllSatResult'
+-- | An 'Data.SBV.allSat' call results in a t'AllSatResult'
 data AllSatResult = AllSatResult { allSatMaxModelCountReached  :: Bool          -- ^ Did we reach the user given model count limit?
                                  , allSatSolverReturnedUnknown :: Bool          -- ^ Did the solver report unknown at the end?
                                  , allSatSolverReturnedDSat    :: Bool          -- ^ Did the solver report delta-satisfiable at the end?
                                  , allSatResults               :: [SMTResult]   -- ^ All satisfying models
                                  }
 
--- | A 'Data.SBV.safe' call results in a 'SafeResult'
-newtype SafeResult   = SafeResult   (Maybe String, String, SMTResult)
+-- | A 'Data.SBV.safe' call results in a t'SafeResult'
+newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
 
 -- | An 'Data.SBV.optimize' call results in a 'OptimizeResult'. In the 'ParetoResult' case, the boolean is 'True'
 -- if we reached pareto-query limit and so there might be more unqueried results remaining. If 'False',
@@ -449,7 +449,7 @@
 getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
 getModelUninterpretedValues s AllSatResult{allSatResults = xs} =  map (s `getModelUninterpretedValue`) xs
 
--- | 'ThmResult' as a generic model provider
+-- | t'ThmResult' as a generic model provider
 instance Modelable ThmResult where
   getModelAssignment (ThmResult r) = getModelAssignment r
   modelExists        (ThmResult r) = modelExists        r
@@ -457,7 +457,7 @@
   getModelObjectives (ThmResult r) = getModelObjectives r
   getModelUIFuns     (ThmResult r) = getModelUIFuns     r
 
--- | 'SatResult' as a generic model provider
+-- | t'SatResult' as a generic model provider
 instance Modelable SatResult where
   getModelAssignment (SatResult r) = getModelAssignment r
   modelExists        (SatResult r) = modelExists        r
diff --git a/Data/SBV/SMT/Utils.hs b/Data/SBV/SMT/Utils.hs
--- a/Data/SBV/SMT/Utils.hs
+++ b/Data/SBV/SMT/Utils.hs
@@ -160,7 +160,7 @@
        skipBar []       = []                     -- Oh dear, line finished, but the string didn't. We're in trouble. Ignore!
 
 -- | An exception thrown from SBV. If the solver ever responds with a non-success value for a command,
--- SBV will throw an 'SBVException', it so the user can process it as required. The provided 'Show' instance
+-- SBV will throw an t'SBVException', it so the user can process it as required. The provided 'Show' instance
 -- will render the failure nicely. Note that if you ever catch this exception, the solver is no longer alive:
 -- You should either -- throw the exception up, or do other proper clean-up before continuing.
 data SBVException = SBVException {
diff --git a/Data/SBV/Tools/KD/KnuckleDragger.hs b/Data/SBV/Tools/KD/KnuckleDragger.hs
--- a/Data/SBV/Tools/KD/KnuckleDragger.hs
+++ b/Data/SBV/Tools/KD/KnuckleDragger.hs
@@ -1184,7 +1184,7 @@
 (=:) = chain
 infixr 1 =:
 
--- | Unicode alternative for `=:`:
+-- | Unicode alternative for `=:`.
 (≡) :: ChainStep a (ChainsTo a) =>  a -> ChainsTo a -> ChainsTo a
 (≡) = (=:)
 infixr 1 ≡
@@ -1213,12 +1213,12 @@
 bs |- ps = (sAnd bs, ps)
 infixl 0 |-
 
--- | Alternative unicode for `|-`:
+-- | Alternative unicode for `|-`.
 (⊢) :: [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
 (⊢) = (|-)
 infixl 0 ⊢
 
--- | Alternative unicode for `??`:
+-- | Alternative unicode for `??`.
 (⁇) :: ProofHint a b => a -> b -> ProofStep a
 (⁇) = (??)
 infixl 2 ⁇
diff --git a/Data/SBV/Tools/KD/Utils.hs b/Data/SBV/Tools/KD/Utils.hs
--- a/Data/SBV/Tools/KD/Utils.hs
+++ b/Data/SBV/Tools/KD/Utils.hs
@@ -142,7 +142,7 @@
                                                                   `seq` rnf getProof
                                                                   `seq` rnf proofName
 
--- | Show instance for 'Proof'
+-- | Show instance for t'Proof'
 instance Show Proof where
   show Proof{rootOfTrust, isUserAxiom, proofName} = '[' : tag ++ "] " ++ proofName
      where tag | isUserAxiom = "Axiom"
diff --git a/Data/SBV/Tools/Range.hs b/Data/SBV/Tools/Range.hs
--- a/Data/SBV/Tools/Range.hs
+++ b/Data/SBV/Tools/Range.hs
@@ -51,7 +51,7 @@
 -- | A range is a pair of boundaries: Lower and upper bounds
 data Range a = Range (Boundary a) (Boundary a)
 
--- | Show instance for 'Range'
+-- | Show instance for t'Range'
 instance Show a => Show (Range a) where
    show (Range l u) = sh True l ++ "," ++ sh False u
      where sh onLeft b = case b of
diff --git a/Data/SBV/Trans.hs b/Data/SBV/Trans.hs
--- a/Data/SBV/Trans.hs
+++ b/Data/SBV/Trans.hs
@@ -124,7 +124,7 @@
   -- ** Soft assumptions
   , assertWithPenalty , Penalty(..)
   -- ** Field extensions
-  -- | If an optimization results in an infinity/epsilon value, the returned `CV` value will be in the corresponding extension field.
+  -- | If an optimization results in an infinity/epsilon value, the returned t'CV' value will be in the corresponding extension field.
   , ExtCV(..), GeneralizedCV(..)
 
   -- * Model extraction
diff --git a/Data/SBV/Trans/Control.hs b/Data/SBV/Trans/Control.hs
--- a/Data/SBV/Trans/Control.hs
+++ b/Data/SBV/Trans/Control.hs
@@ -22,7 +22,7 @@
 
      -- * Querying the solver
      -- ** Extracting values
-     , getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables
+     , getValue, getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables
 
      -- ** Extracting the unsat core
      , getUnsatCore
@@ -74,7 +74,7 @@
 import Data.SBV.Core.Symbolic (MonadQuery(..), QueryT, Query, SymbolicT, QueryContext(..))
 
 import Data.SBV.Control.Query
-import Data.SBV.Control.Utils (queryDebug, executeQuery, getFunction)
+import Data.SBV.Control.Utils (queryDebug, executeQuery, getFunction, getValue)
 
 import Data.SBV.Utils.ExtractIO
 
diff --git a/Data/SBV/Utils/ExtractIO.hs b/Data/SBV/Utils/ExtractIO.hs
--- a/Data/SBV/Utils/ExtractIO.hs
+++ b/Data/SBV/Utils/ExtractIO.hs
@@ -34,18 +34,18 @@
 instance ExtractIO IO where
     extractIO = fmap pure
 
--- | IO extraction for 'MaybeT'.
+-- | IO extraction for t'MaybeT'.
 instance ExtractIO m => ExtractIO (MaybeT m) where
     extractIO = fmap MaybeT . extractIO . runMaybeT
 
--- | IO extraction for 'ExceptT'.
+-- | IO extraction for t'ExceptT'.
 instance ExtractIO m => ExtractIO (ExceptT e m) where
     extractIO = fmap ExceptT . extractIO . runExceptT
 
--- | IO extraction for lazy 'LW.WriterT'.
+-- | IO extraction for lazy t'LW.WriterT'.
 instance (Monoid w, ExtractIO m) => ExtractIO (LW.WriterT w m) where
     extractIO = fmap LW.WriterT . extractIO . LW.runWriterT
 
--- | IO extraction for strict 'SW.WriterT'.
+-- | IO extraction for strict t'SW.WriterT'.
 instance (Monoid w, ExtractIO m) => ExtractIO (SW.WriterT w m) where
     extractIO = fmap SW.WriterT . extractIO . SW.runWriterT
diff --git a/Documentation/SBV/Examples/BitPrecise/Legato.hs b/Documentation/SBV/Examples/BitPrecise/Legato.hs
--- a/Documentation/SBV/Examples/BitPrecise/Legato.hs
+++ b/Documentation/SBV/Examples/BitPrecise/Legato.hs
@@ -81,7 +81,7 @@
 -- Unlike traditional hardware, we assume the program is stored in some other memory area that
 -- we need not model. (No self modifying programs!)
 --
--- 'Mostek' is equipped with an automatically derived 'Mergeable' instance
+-- t'Mostek' is equipped with an automatically derived 'Mergeable' instance
 -- because each field is 'Mergeable'.
 data Mostek = Mostek { memory    :: Memory
                      , registers :: Registers
diff --git a/Documentation/SBV/Examples/Crypto/SHA.hs b/Documentation/SBV/Examples/Crypto/SHA.hs
--- a/Documentation/SBV/Examples/Crypto/SHA.hs
+++ b/Documentation/SBV/Examples/Crypto/SHA.hs
@@ -175,7 +175,7 @@
 -- * Section 5, Preprocessing
 -----------------------------------------------------------------------------
 
--- | 'Block' is a  synonym for lists, but makes the intent clear.
+-- | t'Block' is a  synonym for lists, but makes the intent clear.
 newtype Block a = Block [a]
 
 -- | Prepare the message by turning it into blocks. We also check for the message
diff --git a/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs b/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs
--- a/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs
@@ -71,19 +71,29 @@
 -- We have:
 --
 -- >>> oddSequence2
--- Inductive lemma (strong): oddSequence
---   Base: oddSequence.Base                Q.E.D.
+-- Lemma: oddSequence_0                    Q.E.D.
+-- Lemma: oddSequence_1                    Q.E.D.
+-- Inductive lemma (strong): oddSequence_sNp2
+--   Base: oddSequence_sNp2.Base           Q.E.D.
 --   Asms: 1                               Q.E.D.
---   Step 1: Case split one way:
---     Case [1 of 1]: n[1]                 Q.E.D.
---     Completeness:                       Q.E.D.
+--   Step: 1                               Q.E.D.
+--   Asms: 2                               Q.E.D.
 --   Step: 2                               Q.E.D.
+--   Asms: 3                               Q.E.D.
 --   Step: 3                               Q.E.D.
 --   Step: 4                               Q.E.D.
 --   Step: 5                               Q.E.D.
 --   Step: 6                               Q.E.D.
 --   Step: 7                               Q.E.D.
---   Step: oddSequence.Step                Q.E.D.
+--   Step: oddSequence_sNp2.Step           Q.E.D.
+-- Lemma: oddSequence
+--   Asms  : 1                             Q.E.D.
+--   Step 1: Case split 3 ways:
+--     Case [1 of 3]: n[1]                 Q.E.D.
+--     Case [2 of 3]: n[2]                 Q.E.D.
+--     Case [3 of 3]: n[3]                 Q.E.D.
+--     Completeness:                       Q.E.D.
+--   Result:                               Q.E.D.
 -- [Proven] oddSequence
 oddSequence2 :: IO Proof
 oddSequence2 = runKD $ do
@@ -92,21 +102,31 @@
                                   $ ite (n .== 1) 3
                                   $ 2 * s (n-1) - s (n-2)
 
-  sInduct "oddSequence"
-          (\(Forall @"n" n) -> n .>= 0 .=> s n .== 2 * n + 1) $
-          \ih n -> [n .>= 0] |- s (n+1)
-                             ?? [cases "n" [n+1 .< 2],  hyp (n .>= 0)]
-                             =: let focus v = ite (n+1 .<= 0) 1 (ite (n + 1 .== 1) 3 v)
-                             in focus (2 * s n - s (n-1))
-                             ?? ih `at` Inst @"n" n
-                             =: focus (2 * (2 * n + 1) - s (n - 1))
-                             ?? ih `at` Inst @"n" (n-1)
-                             =: focus (2 * (2 * n + 1) - (2 * (n - 1) + 1))
-                             =: focus (4 * n + 2 - (2 * n - 1))
-                             =: focus (4 * n + 2 - 2 * n + 1)
-                             =: focus (2 * n + 2 + 1)
-                             =: focus (2 * (n + 1) + 1)
-                             =: qed
+  s0 <- lemma "oddSequence_0" (s 0 .== 1) []
+  s1 <- lemma "oddSequence_1" (s 1 .== 3) []
+
+  sNp2 <- sInduct "oddSequence_sNp2"
+                  (\(Forall @"n" n) -> n .>= 2 .=> s n .== 2 * n + 1) $
+                  \ih n -> [n .>= 2] |- s (n+1)                  ?? n .>= 2
+                                     =: 2 * s n - s (n-1)        ?? [hyp (n .>= 2), hprf (ih `at` Inst @"n" n)    ]
+                                     =: 2*(2*n+1) - s (n-1)      ?? [hyp (n .>= 2), hprf (ih `at` Inst @"n" (n-1))]
+                                     =: 2*(2*n+1)-(2*(n-1) + 1)
+                                     =: 4*n+2-(2*n-1)
+                                     =: 4*n+2-2*n+1
+                                     =: 2*n+2+1
+                                     =: 2*(n+1)+1
+                                     =: qed
+
+  calc "oddSequence" (\(Forall @"n" n) -> n .>= 0 .=> s n .== 2 * n + 1) $
+                     \n -> [n .>= 0] |- s n
+                                     ?? [ cases "n" [n .== 0, n .== 1, n .>= 2]
+                                        , hyp (n .>= 0)
+                                        , hprf s0
+                                        , hprf s1
+                                        , hprf $ sNp2 `at` Inst @"n" n
+                                        ]
+                                     =: 2 * n + 1
+                                     =: qed
 
 -- | For strong induction to work, We have to instantiate the proof at a "smaller" value. This
 -- example demonstrates what happens if we don't. We have:
diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
--- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
+++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
@@ -158,7 +158,7 @@
 
 -- * Exists unique
 {- $existsUnique
-We can use the 'ExistsUnique' constructor to indicate a value must exists uniquely. For instance,
+We can use the t'ExistsUnique' constructor to indicate a value must exists uniquely. For instance,
 we can prove that there is an element in 'E' that's less than 'C', but it's not unique. However,
 there's a unique element that's less than all the elements in 'E':
 
diff --git a/Documentation/SBV/Examples/Misc/Newtypes.hs b/Documentation/SBV/Examples/Misc/Newtypes.hs
--- a/Documentation/SBV/Examples/Misc/Newtypes.hs
+++ b/Documentation/SBV/Examples/Misc/Newtypes.hs
@@ -29,13 +29,13 @@
 -- >>> import Data.SBV
 #endif
 
--- | A 'Metres' is a newtype wrapper around 'Integer'.
+-- | A t'Metres' is a newtype wrapper around 'Integer'.
 newtype Metres = Metres Integer deriving (Real, Integral, Num, Enum, Eq, Ord)
 
--- | Symbolic version of 'Metres'.
+-- | Symbolic version of t'Metres'.
 type SMetres   = SBV Metres
 
--- | To use 'Metres' symbolically, we associate it with the underlying symbolic
+-- | To use t'Metres' symbolically, we associate it with the underlying symbolic
 -- type's kind.
 instance HasKind Metres where
    kindOf _ = KUnbounded
@@ -53,10 +53,10 @@
 -- suits our needs.
 newtype HumanHeightInCm = HumanHeightInCm Word16 deriving (Real, Integral, Num, Enum, Eq, Ord)
 
--- | Symbolic version of 'HumanHeightInCm'.
+-- | Symbolic version of t'HumanHeightInCm'.
 type SHumanHeightInCm = SBV HumanHeightInCm
 
--- | Symbolic instance simply follows the underlying type, just like 'Metres'.
+-- | Symbolic instance simply follows the underlying type, just like t'Metres'.
 instance HasKind HumanHeightInCm where
     kindOf _ = KBounded False 16
 
diff --git a/Documentation/SBV/Examples/Transformers/SymbolicEval.hs b/Documentation/SBV/Examples/Transformers/SymbolicEval.hs
--- a/Documentation/SBV/Examples/Transformers/SymbolicEval.hs
+++ b/Documentation/SBV/Examples/Transformers/SymbolicEval.hs
@@ -6,7 +6,7 @@
 -- Maintainer: erkokl@gmail.com
 -- Stability : experimental
 --
--- A demonstration of the use of the 'SymbolicT' and 'QueryT' transformers in
+-- A demonstration of the use of the t'SymbolicT' and t'QueryT' transformers in
 -- the setting of symbolic program evaluation.
 --
 -- In this example, we perform symbolic evaluation across three steps:
@@ -30,8 +30,6 @@
 
 module Documentation.SBV.Examples.Transformers.SymbolicEval where
 
-import Data.SBV (getValue)
-
 import Control.Monad.Except   (Except, ExceptT, MonadError, mapExceptT, runExceptT, throwError)
 import Control.Monad.Identity (Identity(runIdentity))
 import Control.Monad.IO.Class (MonadIO)
@@ -72,7 +70,7 @@
 alloc "" = throwError "tried to allocate unnamed value"
 alloc nm = free nm
 
--- | Allocate an 'Env' holding all input variables for the program.
+-- | Allocate an t'Env' holding all input variables for the program.
 allocEnv :: Alloc Env
 allocEnv = do
     x <- alloc "x"
@@ -133,28 +131,28 @@
 -- output.
 newtype Result = Result SVal
 
--- | Makes a 'Result' from a symbolic value.
+-- | Makes a t'Result' from a symbolic value.
 mkResult :: SBV a -> Result
 mkResult = Result . unSBV
 
--- | Performs symbolic evaluation of a 'Program'.
+-- | Performs symbolic evaluation of a t'Program'.
 runProgramEval :: Env -> Program a -> Except String Result
 runProgramEval env (Program term) = mkResult <$> runEval env term
 
 -- * Property evaluation
 
--- | A property describes a quality of a 'Program'. It is a 'Term' yields a
+-- | A property describes a quality of a t'Program'. It is a 'Term' yields a
 -- boolean value.
 newtype Property = Property (Term Bool)
 
--- | Performs symbolic evaluation of a 'Property.
+-- | Performs symbolic evaluation of a t'Property.
 runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool)
 runPropertyEval (Result res) env (Property term) =
     runEval (env { result = Just res }) term
 
 -- * Checking whether a program satisfies a property
 
--- | The result of 'check'ing the combination of a 'Program' and a 'Property'.
+-- | The result of 'check'ing the combination of a t'Program' and a t'Property'.
 data CheckResult = Proved | Counterexample Integer Integer
     deriving (Eq, Show)
 
@@ -177,7 +175,7 @@
         DSat{} -> throwError "delta-sat"
         Unk    -> throwError "unknown"
 
--- | Checks a 'Property' of a 'Program' (or fails).
+-- | Checks a t'Property' of a t'Program' (or fails).
 check :: Program a -> Property -> IO (Either String CheckResult)
 check program prop = runExceptT $ runSMTWith z3 $ do
     env <- runAlloc allocEnv
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
--- a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
@@ -45,7 +45,7 @@
                    }
                    deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable)
 
--- | Show instance for 'IncS'. The above deriving clause would work just as well,
+-- | Show instance for t'IncS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
 instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (IncS (SBV a)) where
    show (IncS x y) = "{x = " ++ sh x ++ ", y = " ++ sh y ++ "}"
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
--- a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
@@ -48,7 +48,7 @@
                    }
                    deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable)
 
--- | Show instance for 'FibS'. The above deriving clause would work just as well,
+-- | Show instance for t'FibS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
 instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (FibS (SBV a)) where
    show (FibS n i k m) = "{n = " ++ sh n ++ ", i = " ++ sh i ++ ", k = " ++ sh k ++ ", m = " ++ sh m ++ "}"
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
--- a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
@@ -54,7 +54,7 @@
                    }
                    deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable)
 
--- | Show instance for 'GCDS'. The above deriving clause would work just as well,
+-- | Show instance for t'GCDS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
 instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (GCDS (SBV a)) where
    show (GCDS x y i j) = "{x = " ++ sh x ++ ", y = " ++ sh y ++ ", i = " ++ sh i ++ ", j = " ++ sh j ++ "}"
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
--- a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
@@ -38,7 +38,7 @@
                    }
                    deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable)
 
--- | Show instance for 'DivS'. The above deriving clause would work just as well,
+-- | Show instance for t'DivS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
 instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (DivS (SBV a)) where
    show (DivS x y q r) = "{x = " ++ sh x ++ ", y = " ++ sh y ++ ", q = " ++ sh q ++ ", r = " ++ sh r ++ "}"
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
--- a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
@@ -42,7 +42,7 @@
                      }
                      deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable)
 
--- | Show instance for 'SqrtS'. The above deriving clause would work just as well,
+-- | Show instance for t'SqrtS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
 instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (SqrtS (SBV a)) where
    show (SqrtS x sqrt i j) = "{x = " ++ sh x ++ ", sqrt = " ++ sh sqrt ++ ", i = " ++ sh i ++ ", j = " ++ sh j ++ "}"
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
--- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
@@ -44,13 +44,13 @@
                    }
                    deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable)
 
--- | Show instance for 'SumS'. The above deriving clause would work just as well,
+-- | Show instance for t'SumS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
 instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (SumS (SBV a)) where
    show (SumS n i s) = "{n = " ++ sh n ++ ", i = " ++ sh i ++ ", s = " ++ sh s ++ "}"
      where sh v = maybe "<symbolic>" show (unliteral v)
 
--- | 'Queriable instance for our state
+-- | 'Queriable' instance for our state
 instance Queriable IO (SumS SInteger) where
   type QueryResult (SumS SInteger) = SumS Integer
   create = SumS <$> freshVar_ <*> freshVar_ <*> freshVar_
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,7 +1,7 @@
 Cabal-Version: 2.2
 
 Name        : sbv
-Version     : 11.2
+Version     : 11.3
 Category    : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
 Synopsis    : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
 Description : Express properties about Haskell programs and automatically prove them using SMT