diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index cd023be3..b0e51534 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -574,6 +574,7 @@ cmdProveSat isSat str = do
             (t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
             bindItVariable t e
           AllSatResult tevss -> do
+            rPutStrLn (if isSat then "Satisfiable" else "Counterexample")
             let tess = map (map $ \(t,e,_) -> (t,e)) tevss
                 vss  = map (map $ \(_,_,v) -> v)     tevss
             resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
index 05f5f6f4..79afa8f1 100644
--- a/src/Cryptol/Symbolic/SBV.hs
+++ b/src/Cryptol/Symbolic/SBV.hs
@@ -35,6 +35,7 @@ import qualified Control.Exception as X
 import qualified Data.SBV.Dynamic as SBV
 import           Data.SBV (Timing(SaveTiming))
 import           Data.SBV.Internals (showTDiff)
+import           Data.Time (NominalDiffTime)
 
 import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
 import qualified Cryptol.ModuleSystem.Env as M
@@ -88,6 +89,7 @@ proverConfigs =
   , ("sbv-any"      , SBV.defaultSMTCfg )
   ]
 
+-- | The names of all the solvers supported by SBV
 proverNames :: [String]
 proverNames = map fst proverConfigs
 
@@ -104,6 +106,8 @@ satSMTResults (SBV.SatResult r) = [r]
 allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
 allSatSMTResults (SBV.AllSatResult (_, _, _, rs)) = rs
 
+-- | Check if the named solver can be found and invoked
+--   in the current solver environment.
 checkProverInstallation :: String -> IO Bool
 checkProverInstallation s =
   do let prover = lookupProver s
@@ -116,137 +120,227 @@ proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
 proverError msg (_,modEnv) =
   return (Right ((Nothing, ProverError msg), modEnv), [])
 
+
+runSingleProver ::
+  ProverCommand ->
+  [SBV.SMTConfig] ->
+  (SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) ->
+  (res -> [SBV.SMTResult]) ->
+  SBV.Symbolic SBV.SVal ->
+  M.ModuleT IO (Maybe String, [SBV.SMTResult])
+runSingleProver ProverCommand{..} provers callSolver processResult e = do
+  let lPutStrLn = M.withLogger logPutStrLn
+
+  case provers of
+    [prover] -> do
+      when pcVerbose $
+        lPutStrLn $ "Trying proof with " ++
+                                  show (SBV.name (SBV.solver prover))
+      res <- M.io (callSolver prover e)
+      when pcVerbose $
+        lPutStrLn $ "Got result from " ++
+                                  show (SBV.name (SBV.solver prover))
+      return (Just (show (SBV.name (SBV.solver prover))), processResult res)
+    _ ->
+      return ( Nothing
+             , [ SBV.ProofError
+                   prover
+                   [":sat with option prover=any requires option satNum=1"]
+                   Nothing
+               | prover <- provers ]
+             )
+
+runMultiProvers ::
+  ProverCommand ->
+  [SBV.SMTConfig] ->
+  ([SBV.SMTConfig] -> SBV.Symbolic SBV.SVal -> IO (SBV.Solver, NominalDiffTime, res)) ->
+  (res -> [SBV.SMTResult]) ->
+  SBV.Symbolic SBV.SVal ->
+  M.ModuleT IO (Maybe String, [SBV.SMTResult])
+runMultiProvers ProverCommand{..} provers callSolvers processResult e = do
+  let lPutStrLn = M.withLogger logPutStrLn
+
+  when pcVerbose $
+    lPutStrLn $ "Trying proof with " ++
+            intercalate ", " (map (show . SBV.name . SBV.solver) provers)
+  (firstProver, timeElapsed, res) <- M.io (callSolvers provers e)
+  when pcVerbose $
+    lPutStrLn $ "Got result from " ++ show firstProver ++
+                                      ", time: " ++ showTDiff timeElapsed
+  return (Just (show firstProver), processResult res)
+
+-- | Select the appropriate solver or solvers from the given prover command,
+--   and invoke those solvers on the given symbolic value.
+runProver :: ProverCommand -> SBV.Symbolic SBV.SVal -> M.ModuleT IO (Maybe String, [SBV.SMTResult])
+runProver pc@ProverCommand{..} x =
+  do let mSatNum = case pcQueryType of
+                     SatQuery (SomeSat n) -> Just n
+                     SatQuery AllSat -> Nothing
+                     ProveQuery -> Nothing
+
+     provers <-
+       case pcProverName of
+         "any" -> M.io SBV.sbvAvailableSolvers
+         "sbv-any" -> M.io SBV.sbvAvailableSolvers
+         _ -> return [(lookupProver pcProverName)
+                        { SBV.transcript = pcSmtFile
+                        , SBV.allSatMaxModelCount = mSatNum
+                        }]
+
+     let provers' = [ p { SBV.timing = SaveTiming pcProverStats
+                        , SBV.verbose = pcVerbose
+                        , SBV.validateModel = pcValidate
+                        }
+                    | p <- provers
+                    ]
+
+     case pcQueryType of
+        ProveQuery -> runMultiProvers pc provers' SBV.proveWithAny thmSMTResults x
+        SatQuery sn -> case sn of
+          SomeSat 1 -> runMultiProvers pc provers' SBV.satWithAny satSMTResults x
+          _         -> runSingleProver pc provers' SBV.allSatWith allSatSMTResults x
+
+
+-- | Prepare a symbolic query by symbolically simulating the expression found in
+--   the @ProverQuery@.  The result will either be an error or a list of the types
+--   of the symbolic inputs and the symbolic value to supply to the solver.
+--
+--   Note that the difference between sat and prove queries is reflected later
+--   in `runProver` where we call different SBV methods depending on the mode,
+--   so we do _not_ negate the goal here.  Moreover, assumptions are added
+--   using conjunction for sat queries and implication for prove queries.
+--
+--   For safety properties, we want to add them as an additional goal
+--   when we do prove queries, and an additional assumption when we do
+--   sat queries.  In both cases, the safety property is combined with
+--   the main goal via a conjunction.
+prepareQuery ::
+  Eval.EvalOpts ->
+  M.ModuleEnv ->
+  ProverCommand ->
+  IO (Either String ([FinType], SBV.Symbolic SBV.SVal))
+prepareQuery evo modEnv ProverCommand{..} =
+  do let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
+
+     -- The `tyFn` creates variables that are treated as 'forall'
+     -- or 'exists' bound, depending on the sort of query we are doing.
+     let tyFn = case pcQueryType of
+           SatQuery _ -> existsFinType
+           ProveQuery -> forallFinType
+
+     -- The `addAsm` function is used to combine assumptions that
+     -- arise from the types of symbolic variables (e.g. Z n values
+     -- are assumed to be integers in the range `0 <= x < n`) with
+     -- the main content of the query.  We use conjunction or implication
+     -- depending on the type of query.
+     let addAsm = case pcQueryType of
+           ProveQuery -> \x y -> SBV.svOr (SBV.svNot x) y
+           SatQuery _ -> \x y -> SBV.svAnd x y
+
+     let ?evalPrim = evalPrim
+     case predArgTypes pcSchema of
+       Left msg -> return (Left msg)
+       Right ts ->
+         do when pcVerbose $ logPutStrLn (Eval.evalLogger evo) "Simulating..."
+            pure $ Right $ (ts,
+              do -- Compute the symbolic inputs, and any domain constraints needed
+                 -- according to their types.
+                 (args, asms) <- runWriterT (mapM tyFn ts)
+                 -- Run the main symbolic computation.  First we populate the
+                 -- evaluation environment, then we compute the value, finally
+                 -- we apply it to the symbolic inputs.
+                 (safety,b) <- doSBVEval evo $
+                     do env <- Eval.evalDecls SBV extDgs mempty
+                        v <- Eval.evalExpr SBV env pcExpr
+                        Eval.fromVBit <$> foldM Eval.fromVFun v (map pure args)
+                 return (foldr addAsm (SBV.svAnd safety b) asms))
+
+
+-- | Turn the SMT results from SBV into a @ProverResult@ that is ready for the Cryptol REPL.
+--   There may be more than one result if we made a multi-sat query.
+processResults ::
+  Eval.EvalOpts ->
+  ProverCommand ->
+  [FinType] {- ^ Types of the symbolic inputs -} ->
+  [SBV.SMTResult] {- ^ Results from the solver -} ->
+  M.ModuleT IO ProverResult
+processResults evo ProverCommand{..} ts results =
+ do let isSat = case pcQueryType of
+          ProveQuery -> False
+          SatQuery _ -> True
+
+    prims <- M.getPrimMap
+
+    case results of
+       -- allSat can return more than one as long as
+       -- they're satisfiable
+       (SBV.Satisfiable {} : _) -> do
+         tevss <- mapM mkTevs results
+         return $ AllSatResult tevss
+         where
+           mkTevs result = do
+             let Right (_, cvs) = SBV.getModelAssignment result
+                 (vs, _) = parseValues ts cvs
+                 sattys = unFinType <$> ts
+             satexprs <-
+               doEval evo (zipWithM (Concrete.toExpr prims) sattys vs)
+             case zip3 sattys <$> (sequence satexprs) <*> pure vs of
+               Nothing ->
+                 panic "Cryptol.Symbolic.sat"
+                   [ "unable to make assignment into expression" ]
+               Just tevs -> return $ tevs
+
+       -- prove returns only one
+       [SBV.Unsatisfiable {}] ->
+         return $ ThmResult (unFinType <$> ts)
+
+       -- unsat returns empty
+       [] -> return $ ThmResult (unFinType <$> ts)
+
+       -- otherwise something is wrong
+       _ -> return $ ProverError (rshow results)
+              where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)
+                          | otherwise = show . SBV.ThmResult . head
+
+-- | Execute a symbolic ':prove' or ':sat' command.
+--
+--   This command returns a pair: the first element is the name of the
+--   solver that completes the given query (if any) along with the result
+--   of executing the query.
 satProve :: ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)
-satProve ProverCommand {..} =
+satProve pc@ProverCommand {..} =
   protectStack proverError $ \(evo,modEnv) ->
 
   M.runModuleM (evo,modEnv) $ do
-  let (isSat, mSatNum) = case pcQueryType of
-        ProveQuery -> (False, Nothing)
-        SatQuery sn -> case sn of
-          SomeSat n -> (True, Just n)
-          AllSat    -> (True, Nothing)
-  let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
-  provers <-
-    case pcProverName of
-      "any" -> M.io SBV.sbvAvailableSolvers
-      "sbv-any" -> M.io SBV.sbvAvailableSolvers
-      _ -> return [(lookupProver pcProverName) { SBV.transcript = pcSmtFile
-                                               , SBV.allSatMaxModelCount = mSatNum
-                                               }]
 
-
-  let provers' = [ p { SBV.timing = SaveTiming pcProverStats
-                     , SBV.verbose = pcVerbose
-                     , SBV.validateModel = pcValidate
-                     } | p <- provers ]
-  let tyFn = if isSat then existsFinType else forallFinType
-  let lPutStrLn = M.withLogger logPutStrLn
-  let runProver fn tag e = do
-        case provers of
-          [prover] -> do
-            when pcVerbose $
-              lPutStrLn $ "Trying proof with " ++
-                                        show (SBV.name (SBV.solver prover))
-            res <- M.io (fn prover e)
-            when pcVerbose $
-              lPutStrLn $ "Got result from " ++
-                                        show (SBV.name (SBV.solver prover))
-            return (Just (show (SBV.name (SBV.solver prover))), tag res)
-          _ ->
-            return ( Nothing
-                   , [ SBV.ProofError
-                         prover
-                         [":sat with option prover=any requires option satNum=1"]
-                         Nothing
-                     | prover <- provers ]
-                   )
-      runProvers fn tag e = do
-        when pcVerbose $
-          lPutStrLn $ "Trying proof with " ++
-                  intercalate ", " (map (show . SBV.name . SBV.solver) provers)
-        (firstProver, timeElapsed, res) <- M.io (fn provers' e)
-        when pcVerbose $
-          lPutStrLn $ "Got result from " ++ show firstProver ++
-                                            ", time: " ++ showTDiff timeElapsed
-        return (Just (show firstProver), tag res)
-  let runFn = case pcQueryType of
-        ProveQuery -> runProvers SBV.proveWithAny thmSMTResults
-        SatQuery sn -> case sn of
-          SomeSat 1 -> runProvers SBV.satWithAny satSMTResults
-          _         -> runProver SBV.allSatWith allSatSMTResults
-  let addAsm = case pcQueryType of
-        ProveQuery -> \x y -> SBV.svOr (SBV.svNot x) y
-        SatQuery _ -> \x y -> SBV.svAnd x y
-
-  let ?evalPrim = evalPrim
-  case predArgTypes pcSchema of
+  M.io (prepareQuery evo modEnv pc) >>= \case
     Left msg -> return (Nothing, ProverError msg)
-    Right ts -> do when pcVerbose $ lPutStrLn "Simulating..."
-                   (_,v) <- doSBVEval evo $
-                              do env <- Eval.evalDecls SBV extDgs mempty
-                                 Eval.evalExpr SBV env pcExpr
-                   prims <- M.getPrimMap
-                   runRes <- runFn $ do
-                               (args, asms) <- runWriterT (mapM tyFn ts)
-                               (_,b) <- doSBVEval evo (Eval.fromVBit <$>
-                                          foldM Eval.fromVFun v (map pure args))
-                               return (foldr addAsm b asms)
-                   let (firstProver, results) = runRes
-                   esatexprs <- case results of
-                     -- allSat can return more than one as long as
-                     -- they're satisfiable
-                     (SBV.Satisfiable {} : _) -> do
-                       tevss <- mapM mkTevs results
-                       return $ AllSatResult tevss
-                       where
-                         mkTevs result = do
-                           let Right (_, cvs) = SBV.getModelAssignment result
-                               (vs, _) = parseValues ts cvs
-                               sattys = unFinType <$> ts
-                           satexprs <-
-                             doEval evo (zipWithM (Concrete.toExpr prims) sattys vs)
-                           case zip3 sattys <$> (sequence satexprs) <*> pure vs of
-                             Nothing ->
-                               panic "Cryptol.Symbolic.sat"
-                                 [ "unable to make assignment into expression" ]
-                             Just tevs -> return $ tevs
-                     -- prove returns only one
-                     [SBV.Unsatisfiable {}] ->
-                       return $ ThmResult (unFinType <$> ts)
-                     -- unsat returns empty
-                     [] -> return $ ThmResult (unFinType <$> ts)
-                     -- otherwise something is wrong
-                     _ -> return $ ProverError (rshow results)
-                            where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)
-                                        | otherwise = show . SBV.ThmResult . head
-                   return (firstProver, esatexprs)
+    Right (ts, q) ->
+      do (firstProver, results) <- runProver pc q
+         esatexprs <- processResults evo pc ts results
+         return (firstProver, esatexprs)
 
+-- | Execute a symbolic ':prove' or ':sat' command when the prover is
+--   set to offline.  This only prepares the SMT input file for the
+--   solver and does not actually invoke the solver.
+--
+--   This method returns either an error message or the text of
+--   the SMT input file corresponding to the given prover command.
 satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
-satProveOffline ProverCommand {..} =
+satProveOffline pc@ProverCommand {..} =
   protectStack (\msg (_,modEnv) -> return (Right (Left msg, modEnv), [])) $
   \(evOpts,modEnv) -> do
     let isSat = case pcQueryType of
           ProveQuery -> False
           SatQuery _ -> True
-    let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
-    let tyFn = if isSat then existsFinType else forallFinType
-    let addAsm = if isSat then SBV.svAnd else \x y -> SBV.svOr (SBV.svNot x) y
-    let ?evalPrim = evalPrim
-    case predArgTypes pcSchema of
+
+    prepareQuery evOpts modEnv pc >>= \case
       Left msg -> return (Right (Left msg, modEnv), [])
-      Right ts ->
-        do when pcVerbose $ logPutStrLn (Eval.evalLogger evOpts) "Simulating..."
-           (_,v) <- doSBVEval evOpts $
-                      do env <- Eval.evalDecls SBV extDgs mempty
-                         Eval.evalExpr SBV env pcExpr
-           smtlib <- SBV.generateSMTBenchmark isSat $ do
-             (args, asms) <- runWriterT (mapM tyFn ts)
-             (_,b) <- doSBVEval evOpts
-                          (Eval.fromVBit <$> foldM Eval.fromVFun v (map pure args))
-             return (foldr addAsm b asms)
+      Right (_ts, q) ->
+        do smtlib <- SBV.generateSMTBenchmark isSat q
            return (Right (Right smtlib, modEnv), [])
 
+
 protectStack :: (String -> M.ModuleCmd a)
              -> M.ModuleCmd a
              -> M.ModuleCmd a
@@ -257,12 +351,18 @@ protectStack mkErr cmd modEnv =
         msg = "Symbolic evaluation failed to terminate."
         handler () = mkErr msg modEnv
 
+-- | Given concrete values from the solver and a collection of finite types,
+--   reconstruct Cryptol concrete values, and return any unused solver
+--   values.
 parseValues :: [FinType] -> [SBV.CV] -> ([Concrete.Value], [SBV.CV])
 parseValues [] cvs = ([], cvs)
 parseValues (t : ts) cvs = (v : vs, cvs'')
   where (v, cvs') = parseValue t cvs
         (vs, cvs'') = parseValues ts cvs'
 
+-- | Parse a single value of a finite type by consuming some number of
+--   solver values.  The parsed Cryptol values is returned along with
+--   any solver values not consumed.
 parseValue :: FinType -> [SBV.CV] -> (Concrete.Value, [SBV.CV])
 parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
 parseValue FTBit (cv : cvs) = (Eval.VBit (SBV.cvToBool cv), cvs)
diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs
index 9c752330..d82e9953 100644
--- a/src/Cryptol/Transform/Specialize.hs
+++ b/src/Cryptol/Transform/Specialize.hs
@@ -324,7 +324,7 @@ instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
 instantiateExpr [] 0 e = return e
 instantiateExpr [] n (EProofAbs _ e) = instantiateExpr [] (n - 1) e
 instantiateExpr (t : ts) n (ETAbs param e) =
-  instantiateExpr ts n (apSubst (singleSubst (tpVar param) t) e)
+  instantiateExpr ts n (apSubst (singleTParamSubst param t) e)
 instantiateExpr _ _ _ = fail "instantiateExpr: wrong number of type/proof arguments"
 
 
diff --git a/src/Cryptol/TypeCheck/Default.hs b/src/Cryptol/TypeCheck/Default.hs
index e1305646..2331246a 100644
--- a/src/Cryptol/TypeCheck/Default.hs
+++ b/src/Cryptol/TypeCheck/Default.hs
@@ -9,7 +9,7 @@ import Control.Monad(guard)
 import Cryptol.TypeCheck.Type
 import Cryptol.TypeCheck.SimpType(tMax,tWidth)
 import Cryptol.TypeCheck.Error(Warning(..))
-import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,singleSubst)
+import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst)
 import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
 import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
 import Cryptol.Utils.Panic(panic)
@@ -152,7 +152,7 @@ improveByDefaultingWithPure as ps =
           let ty  = case ts of
                       [] -> tNum (0::Int)
                       _  -> foldr1 tMax ts
-              su1 = singleSubst x ty
+              su1 = uncheckedSingleSubst x ty
           in ( (x,ty) : [ (y,apSubst su1 t) | (y,t) <- yes ]
              , no         -- We know that `x` does not appear here
              , otherFree  -- We know that `x` did not appear here either
diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
index eb3755f5..4dcaea65 100644
--- a/src/Cryptol/TypeCheck/Monad.hs
+++ b/src/Cryptol/TypeCheck/Monad.hs
@@ -550,13 +550,7 @@ extendSubst su =
             , "Type:     " ++ show (pp ty)
             ]
         TVFree _ _ tvs _ ->
-          do let bounds tv =
-                   case tv of
-                     TVBound tp -> Set.singleton tp
-                     TVFree _ _ tps _ -> tps
-             let vars = Set.unions (map bounds (Set.elems (fvs ty)))
-                 -- (Set.filter isBoundTV (fvs ty))
-             let escaped = Set.difference vars tvs
+          do let escaped = Set.difference (freeParams ty) tvs
              if Set.null escaped then return () else
                panic "Cryptol.TypeCheck.Monad.extendSubst"
                  [ "Escaped quantified variables:"
diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs
index c06791b2..74a87924 100644
--- a/src/Cryptol/TypeCheck/Sanity.hs
+++ b/src/Cryptol/TypeCheck/Sanity.hs
@@ -17,7 +17,7 @@ module Cryptol.TypeCheck.Sanity
 
 import Cryptol.Parser.Position(thing)
 import Cryptol.TypeCheck.AST
-import Cryptol.TypeCheck.Subst (apSubst, singleSubst)
+import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst)
 import Cryptol.TypeCheck.Monad(InferInput(..))
 import Cryptol.Utils.Ident
 
@@ -221,7 +221,7 @@ exprSchema expr =
                 let k' = kindOf a
                 unless (k == k') $ reportError $ KindMismatch k' k
 
-                let su = singleSubst (tpVar a) t
+                let su = singleTParamSubst a t
                 return $ Forall as (apSubst su ps) (apSubst su t1)
 
            Forall [] _ _ -> reportError BadInstantiation
diff --git a/src/Cryptol/TypeCheck/Solver/Improve.hs b/src/Cryptol/TypeCheck/Solver/Improve.hs
index 5976e860..de0bd111 100644
--- a/src/Cryptol/TypeCheck/Solver/Improve.hs
+++ b/src/Cryptol/TypeCheck/Solver/Improve.hs
@@ -51,7 +51,7 @@ improveLit impSkol prop =
      (_,b) <- aSeq t
      a     <- aTVar b
      unless impSkol $ guard (isFreeTV a)
-     let su = singleSubst a tBit
+     let su = uncheckedSingleSubst a tBit
      return (su, [])
 
 
@@ -66,13 +66,15 @@ improveEq impSkol fins prop =
   where
   rewrite this other =
     do x <- aTVar this
-       guard (considerVar x && x `Set.notMember` fvs other)
-       return (singleSubst x other, [])
+       guard (considerVar x)
+       case singleSubst x other of
+         Left _ -> mzero
+         Right su -> return (su, [])
     <|>
     do (v,s) <- isSum this
-       guard (v `Set.notMember` fvs other)
-       return (singleSubst v (Mk.tSub other s), [ other >== s ])
-
+       case singleSubst v (Mk.tSub other s) of
+         Left _ -> mzero
+         Right su -> return (su, [ other >== s ])
 
   isSum t = do (v,s) <- matches t (anAdd, aTVar, __)
                valid v s
diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs
index 1dc62cc6..208045e6 100644
--- a/src/Cryptol/TypeCheck/Subst.hs
+++ b/src/Cryptol/TypeCheck/Subst.hs
@@ -14,7 +14,10 @@
 module Cryptol.TypeCheck.Subst
   ( Subst
   , emptySubst
+  , SubstError(..)
   , singleSubst
+  , singleTParamSubst
+  , uncheckedSingleSubst
   , (@@)
   , defaultingSubst
   , listSubst
@@ -47,12 +50,22 @@ import Cryptol.Utils.Misc(anyJust)
 -- | A 'Subst' value represents a substitution that maps each 'TVar'
 -- to a 'Type'.
 --
--- Invariant: If there is a mapping from @TVFree _ _ tps _@ to a type
--- @t@, then @t@ must not mention (directly or indirectly) any type
--- parameter that is not in @tps@. In particular, if @t@ contains a
--- variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
+-- Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a
+-- type @t@, then @t@ must not mention (directly or indirectly) any
+-- type parameter that is not in @tps@. In particular, if @t@ contains
+-- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
 -- @tps@. This ensures that applying the substitution will not permit
 -- any type parameter to escape from its scope.
+--
+-- Invariant 2: The substitution must be idempotent, in that applying
+-- a substitution to any 'Type' in the map should leave that 'Type'
+-- unchanged. In other words, 'Type' values in the range of a 'Subst'
+-- should not mention any 'TVar' in the domain of the 'Subst'. In
+-- particular, this implies that a substitution must not contain any
+-- recursive variable mappings.
+--
+-- Invariant 3: The substitution must be kind correct: Each 'TVar' in
+-- the substitution must map to a 'Type' of the same kind.
 
 data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type))
                , suBoundMap :: !(IntMap.IntMap (TVar, Type))
@@ -67,18 +80,42 @@ emptySubst =
     , suDefaulting = False
     }
 
-singleSubst :: TVar -> Type -> Subst
-singleSubst v@(TVFree i _ _tps _) t =
+-- | Reasons to reject a single-variable substitution.
+data SubstError
+  = SubstRecursive
+  -- ^ 'TVar' maps to a type containing the same variable.
+  | SubstEscaped [TParam]
+  -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.
+  | SubstKindMismatch Kind Kind
+  -- ^ 'TVar' maps to a type with a different kind.
+
+singleSubst :: TVar -> Type -> Either SubstError Subst
+singleSubst x t
+  | kindOf x /= kindOf t   = Left (SubstKindMismatch (kindOf x) (kindOf t))
+  | x `Set.member` fvs t   = Left SubstRecursive
+  | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped))
+  | otherwise              = Right (uncheckedSingleSubst x t)
+  where
+    escaped =
+      case x of
+        TVBound _ -> Set.empty
+        TVFree _ _ scope _ -> freeParams t `Set.difference` scope
+
+uncheckedSingleSubst :: TVar -> Type -> Subst
+uncheckedSingleSubst v@(TVFree i _ _tps _) t =
   S { suFreeMap = IntMap.singleton i (v, t)
     , suBoundMap = IntMap.empty
     , suDefaulting = False
     }
-singleSubst v@(TVBound tp) t =
+uncheckedSingleSubst v@(TVBound tp) t =
   S { suFreeMap = IntMap.empty
     , suBoundMap = IntMap.singleton (tpUnique tp) (v, t)
     , suDefaulting = False
     }
 
+singleTParamSubst :: TParam -> Type -> Subst
+singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t
+
 (@@) :: Subst -> Subst -> Subst
 s2 @@ s1
   | isEmptySubst s2 =
@@ -327,4 +364,3 @@ instance TVars DeclDef where
 
 instance TVars Module where
   apSubst su m = m { mDecls = apSubst su (mDecls m) }
-
diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs
index f421bdcd..3b90eea1 100644
--- a/src/Cryptol/TypeCheck/Type.hs
+++ b/src/Cryptol/TypeCheck/Type.hs
@@ -677,6 +677,12 @@ pError msg = TCon (TError KProp msg) []
 noFreeVariables :: FVS t => t -> Bool
 noFreeVariables = all (not . isFreeTV) . Set.toList . fvs
 
+freeParams :: FVS t => t -> Set TParam
+freeParams x = Set.unions (map params (Set.toList (fvs x)))
+  where
+    params (TVFree _ _ tps _) = tps
+    params (TVBound tp) = Set.singleton tp
+
 class FVS t where
   fvs :: t -> Set TVar
 
@@ -827,9 +833,10 @@ instance PP (WithNames Type) where
           (PEqual, [t1,t2])   -> go 0 t1 <+> text "==" <+> go 0 t2
           (PNeq ,  [t1,t2])   -> go 0 t1 <+> text "!=" <+> go 0 t2
           (PGeq,  [t1,t2])    -> go 0 t1 <+> text ">=" <+> go 0 t2
-          (PFin,  [t1])       -> text "fin" <+> (go 4 t1)
+          (PFin,  [t1])       -> optParens (prec > 3) $ text "fin" <+> (go 4 t1)
           (PHas x, [t1,t2])   -> ppSelector x <+> text "of"
                                <+> go 0 t1 <+> text "is" <+> go 0 t2
+          (PAnd, [t1,t2])     -> parens (commaSep (map (go 0) (t1 : pSplitAnd t2)))
 
           (PRing, [t1])       -> pp pc <+> go 4 t1
           (PField, [t1])      -> pp pc <+> go 4 t1
@@ -840,7 +847,7 @@ instance PP (WithNames Type) where
           (PSignedCmp, [t1])  -> pp pc <+> go 4 t1
           (PLiteral, [t1,t2]) -> pp pc <+> go 4 t1 <+> go 4 t2
 
-          (_, _)              -> pp pc <+> fsep (map (go 4) ts)
+          (_, _)              -> optParens (prec > 3) $ pp pc <+> fsep (map (go 4) ts)
 
       TCon f ts -> optParens (prec > 3)
                 $ pp f <+> fsep (map (go 4) ts)
diff --git a/src/Cryptol/TypeCheck/TypeOf.hs b/src/Cryptol/TypeCheck/TypeOf.hs
index 75ba5d53..2ff5801f 100644
--- a/src/Cryptol/TypeCheck/TypeOf.hs
+++ b/src/Cryptol/TypeCheck/TypeOf.hs
@@ -68,7 +68,7 @@ fastSchemaOf tyenv expr =
     ETApp e t      -> case fastSchemaOf tyenv e of
                         Forall (tparam : tparams) props ty
                           -> Forall tparams (map (plainSubst s) props) (plainSubst s ty)
-                          where s = singleSubst (tpVar tparam) t
+                          where s = singleTParamSubst tparam t
                         _ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
                                [ "ETApp body with no type parameters" ]
                         -- When calling 'fastSchemaOf' on a
diff --git a/src/Cryptol/TypeCheck/Unify.hs b/src/Cryptol/TypeCheck/Unify.hs
index c0793757..92f2b50e 100644
--- a/src/Cryptol/TypeCheck/Unify.hs
+++ b/src/Cryptol/TypeCheck/Unify.hs
@@ -110,22 +110,21 @@ bindVar v@(TVBound {}) t
   | otherwise     = uniError $ UniKindMismatch k (kindOf t)
   where k = kindOf v
 
-bindVar x@(TVFree _ _ xscope _) (TVar y@(TVFree _ _ yscope _))
-  | xscope `Set.isProperSubsetOf` yscope = return (singleSubst y (TVar x), [])
+bindVar x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _))
+  | xscope `Set.isProperSubsetOf` yscope, xk == yk =
+    return (uncheckedSingleSubst y (TVar x), [])
+    -- In this case, we can add the reverse binding y ~> x to the
+    -- substitution, but the instantiation x ~> y would be forbidden
+    -- because it would allow y to escape from its scope.
 
-bindVar x@(TVFree _ k inScope _d) t
-  | not (k == kindOf t)     = uniError $ UniKindMismatch k (kindOf t)
-  | recTy && k == KType     = uniError $ UniRecursive x t
-  | not (Set.null escaped)  = uniError $ UniNonPolyDepends x $ Set.toList escaped
-  | recTy                   = return (emptySubst, [TVar x =#= t])
-  | otherwise               = return (singleSubst x t, [])
-    where
-    escaped = freeParams t `Set.difference` inScope
-    recTy   = x `Set.member` fvs t
-
-
-freeParams :: FVS t => t -> Set.Set TParam
-freeParams x = Set.unions (map params (Set.toList (fvs x)))
-  where
-    params (TVFree _ _ tps _) = tps
-    params (TVBound tp) = Set.singleton tp
+bindVar x t =
+  case singleSubst x t of
+    Left SubstRecursive
+      | kindOf x == KType -> uniError $ UniRecursive x t
+      | otherwise -> return (emptySubst, [TVar x =#= t])
+    Left (SubstEscaped tps) ->
+      uniError $ UniNonPolyDepends x tps
+    Left (SubstKindMismatch k1 k2) ->
+      uniError $ UniKindMismatch k1 k2
+    Right su ->
+      return (su, [])
diff --git a/tests/issues/issue066.icry.stdout b/tests/issues/issue066.icry.stdout
index c77a7c23..7d16f87b 100644
--- a/tests/issues/issue066.icry.stdout
+++ b/tests/issues/issue066.icry.stdout
@@ -4,10 +4,12 @@ it : {result : Bit, arg1 : [4]}
 
 Run-time error: no counterexample available
 True
+Counterexample
 f 0xc = False
 it : {result : Bit, arg1 : [4]}
 {arg1 = 0xc, result = False}
 False
+Satisfiable
 f 0x3 = True
 it : {result : Bit, arg1 : [4]}
 {arg1 = 0x3, result = True}
@@ -16,17 +18,21 @@ Unsatisfiable
 it : {result : Bit, arg1 : [4]}
 
 Run-time error: no satisfying assignment available
+Counterexample
 g {x = 0xffffffff, y = 0x00000000} = False
 it : {result : Bit, arg1 : {x : [32], y : [32]}}
 {arg1 = {x = 0xffffffff, y = 0x00000000}, result = False}
+Satisfiable
 g {x = 0x00000000, y = 0x00000000} = True
 it : {result : Bit, arg1 : {x : [32], y : [32]}}
 {arg1 = {x = 0x00000000, y = 0x00000000}, result = True}
+Counterexample
 h 0x00 0x00 = False
 it : {result : Bit, arg1 : [8], arg2 : [8]}
 {arg1 = 0x00, arg2 = 0x00, result = False}
 0x00
 0x00
+Satisfiable
 h 0x00 0x01 = True
 it : {result : Bit, arg1 : [8], arg2 : [8]}
 {arg1 = 0x00, arg2 = 0x01, result = True}
diff --git a/tests/issues/issue072.icry.stdout b/tests/issues/issue072.icry.stdout
index f61475b5..0c8e044f 100644
--- a/tests/issues/issue072.icry.stdout
+++ b/tests/issues/issue072.icry.stdout
@@ -1,6 +1,9 @@
 Loading module Cryptol
+Satisfiable
 it : {result : Bit, arg1 : [4]}
+Satisfiable
 it : [11]{result : Bit, arg1 : [4]}
 must be an integer > 0 or "all"
 must be an integer > 0 or "all"
+Satisfiable
 it : [3]{result : Bit, arg1 : [4]}
diff --git a/tests/issues/issue093.icry.stdout b/tests/issues/issue093.icry.stdout
index 83bf89e2..5b102a55 100644
--- a/tests/issues/issue093.icry.stdout
+++ b/tests/issues/issue093.icry.stdout
@@ -19,12 +19,16 @@ Testing... f0 = False
 :prove t2
 	Q.E.D.
 :prove f0
-	f0 = False
+	Counterexample
+f0 = False
 :sat t0
-	t0 = True
+	Satisfiable
+t0 = True
 :sat t1
-	t1 0x00000000 = True
+	Satisfiable
+t1 0x00000000 = True
 :sat t2
-	t2 0xfffffffe 0xffffffff = True
+	Satisfiable
+t2 0xfffffffe 0xffffffff = True
 :sat f0
 	Unsatisfiable
diff --git a/tests/issues/issue135.icry.stdout b/tests/issues/issue135.icry.stdout
index 74d93f7a..7fc651fd 100644
--- a/tests/issues/issue135.icry.stdout
+++ b/tests/issues/issue135.icry.stdout
@@ -1,3 +1,4 @@
 Loading module Cryptol
+Satisfiable
 (\(x : Bit) (y : Bit) -> x < y) False True = True
 Q.E.D.
diff --git a/tests/issues/issue148.icry.stdout b/tests/issues/issue148.icry.stdout
index 47012694..55ba47bb 100644
--- a/tests/issues/issue148.icry.stdout
+++ b/tests/issues/issue148.icry.stdout
@@ -1,4 +1,5 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
+Satisfiable
 (\(e : [64]) -> (e @@ [8 .. 24]) != zero) 0x00feff8000000000 = True
diff --git a/tests/issues/issue407.icry.stdout b/tests/issues/issue407.icry.stdout
index cb29eb08..ed1d2523 100644
--- a/tests/issues/issue407.icry.stdout
+++ b/tests/issues/issue407.icry.stdout
@@ -3,6 +3,7 @@ Loading module Cryptol
  [False, False, False, False, True, ...],
  [False, False, True, True, False, ...],
  [False, True, False, True, False, ...]]
+Counterexample
 (\(x : [4]) -> (transpose [x ...]) @ 0 @ 0 == False) 0x8 = False
 Q.E.D.
 Q.E.D.
diff --git a/tests/issues/issue474.icry.stdout b/tests/issues/issue474.icry.stdout
index 74c8d6a4..50c8b5e9 100644
--- a/tests/issues/issue474.icry.stdout
+++ b/tests/issues/issue474.icry.stdout
@@ -1,2 +1,3 @@
 Loading module Cryptol
+Satisfiable
 (\x -> mapped x == 'N') 0x41 = True
diff --git a/tests/issues/issue702.icry.stdout b/tests/issues/issue702.icry.stdout
index 2b81cffe..c0481ea2 100644
--- a/tests/issues/issue702.icry.stdout
+++ b/tests/issues/issue702.icry.stdout
@@ -1,5 +1,7 @@
 Loading module Cryptol
+Satisfiable
 (\(x : {b : Bit, a : Bit}) -> x.a && x.b)
   {a = True, b = True} = True
+Satisfiable
 (\(x : {b : [8], a : Bit}) -> x.b == 0 /\ x.a)
   {a = True, b = 0x00} = True
diff --git a/tests/issues/issue723.cry b/tests/issues/issue723.cry
new file mode 100644
index 00000000..0ce7dc7f
--- /dev/null
+++ b/tests/issues/issue723.cry
@@ -0,0 +1,7 @@
+f : {n} (fin n) => [n] -> [n]
+f x = g x
+  where
+    m1 = zero # x
+
+    g : {k} (fin k) => [k] -> [k]
+    g m0 = m0 ^ m1
diff --git a/tests/issues/issue723.icry b/tests/issues/issue723.icry
new file mode 100644
index 00000000..ed91f861
--- /dev/null
+++ b/tests/issues/issue723.icry
@@ -0,0 +1 @@
+:l issue723.cry
diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout
new file mode 100644
index 00000000..763b8421
--- /dev/null
+++ b/tests/issues/issue723.icry.stdout
@@ -0,0 +1,20 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+[warning] at issue723.cry:4:10--4:18:
+  Defaulting type argument 'front' of '(#)' to 0
+
+[error] at issue723.cry:7:5--7:19:
+  Failed to validate user-specified signature.
+    in the definition of 'Main::g', at issue723.cry:7:5--7:6,
+    we need to show that
+      for any type k
+      assuming
+        • fin k
+      the following constraints hold:
+        • k >= n`908
+            arising from
+            matching types
+            at issue723.cry:7:17--7:19
+  where
+  n`908 is signature variable 'n' at issue723.cry:1:6--1:7
diff --git a/tests/issues/issue725.icry b/tests/issues/issue725.icry
new file mode 100644
index 00000000..836eb604
--- /dev/null
+++ b/tests/issues/issue725.icry
@@ -0,0 +1,14 @@
+:set show-examples = no
+:set prover-stats=no
+
+:set prover=z3
+
+:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
+:sat \(a:[8], b:[8]) -> a == ~zero /\ a@b == False
+:prove \(a:[8], b:[8]) -> a == zero ==> a@b == False
+
+:set prover=w4-z3
+
+:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
+:sat \(a:[8], b:[8]) -> a == ~zero /\ a@b == False
+:prove \(a:[8], b:[8]) -> a == zero ==> a@b == False
diff --git a/tests/issues/issue725.icry.stdout b/tests/issues/issue725.icry.stdout
new file mode 100644
index 00000000..600419a6
--- /dev/null
+++ b/tests/issues/issue725.icry.stdout
@@ -0,0 +1,9 @@
+Loading module Cryptol
+
+operation can not be supported on symbolic values: integer exponentiation
+Unsatisfiable
+Counterexample
+
+operation can not be supported on symbolic values: integer exponentiation
+Unsatisfiable
+Counterexample
diff --git a/tests/issues/issue731.cry b/tests/issues/issue731.cry
new file mode 100644
index 00000000..726a6605
--- /dev/null
+++ b/tests/issues/issue731.cry
@@ -0,0 +1,7 @@
+type constraint T n = (fin n, n >= 1)
+
+type constraint Both p q = (p, q)
+
+type constraint Fin2 i j = Both (fin i) (fin j)
+
+type constraint i <=> j = (i <= j, i >= j)
diff --git a/tests/issues/issue731.icry b/tests/issues/issue731.icry
new file mode 100644
index 00000000..241ac198
--- /dev/null
+++ b/tests/issues/issue731.icry
@@ -0,0 +1,2 @@
+:l issue731.cry
+:browse Main
diff --git a/tests/issues/issue731.icry.stdout b/tests/issues/issue731.icry.stdout
new file mode 100644
index 00000000..970bf839
--- /dev/null
+++ b/tests/issues/issue731.icry.stdout
@@ -0,0 +1,14 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Constraint Synonyms
+===================
+
+  Public
+  ------
+
+    type constraint (<=>) i j = (i <= j, i >= j)
+    type constraint Both p q = (p, q)
+    type constraint Fin2 i j = Both (fin i) (fin j)
+    type constraint T n = (fin n, n >= 1)
+
diff --git a/tests/issues/trac289.icry.stdout b/tests/issues/trac289.icry.stdout
index 562e81da..83ddb214 100644
--- a/tests/issues/trac289.icry.stdout
+++ b/tests/issues/trac289.icry.stdout
@@ -2,5 +2,6 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 Q.E.D.
+Counterexample
 av1 0xfdffffe0 0x7fffffe0 = False
 Q.E.D.
diff --git a/tests/regression/r03.icry.stdout b/tests/regression/r03.icry.stdout
index 1fe1993b..06808745 100644
--- a/tests/regression/r03.icry.stdout
+++ b/tests/regression/r03.icry.stdout
@@ -1,4 +1,6 @@
 Loading module Cryptol
 Loading module r03
+Satisfiable
 True
+Counterexample
 False