diff --git a/heapster-saw/examples/Makefile b/heapster-saw/examples/Makefile
index dee6e52df7..dc91dd7a13 100644
--- a/heapster-saw/examples/Makefile
+++ b/heapster-saw/examples/Makefile
@@ -1,4 +1,4 @@
-all: Makefile.coq
+all: Makefile.coq mr-solver-tests
 
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
@@ -32,3 +32,12 @@ rust_data.bc: rust_data.rs
 
 rust_lifetimes.bc: rust_lifetimes.rs
 	rustc --crate-type=lib --emit=llvm-bc rust_lifetimes.rs
+
+# Lists all the Mr Solver tests, without their ".saw" suffix
+MR_SOLVER_TESTS = arrays_mr_solver
+
+.PHONY: mr-solver-tests $(MR_SOLVER_TESTS)
+mr-solver-tests: $(MR_SOLVER_TESTS)
+
+$(MR_SOLVER_TESTS):
+	$(SAW) $@.saw
diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw
index 0326bac2ec..838e1d2874 100644
--- a/heapster-saw/examples/arrays_mr_solver.saw
+++ b/heapster-saw/examples/arrays_mr_solver.saw
@@ -1,3 +1,19 @@
 include "arrays.saw";
+
+let eq_bool b1 b2 =
+  if b1 then
+    if b2 then true else false
+  else
+    if b2 then false else true;
+
+let fail = do { print "Test failed"; exit 1; };
+let run_test name test expected =
+  do { if expected then print (str_concat "Test: " name) else
+         print (str_concat (str_concat "Test: " name) " (expecting failure)");
+       actual <- test;
+       if eq_bool actual expected then print "Success\n" else
+         do { print "Test failed\n"; exit 1; }; };
+
+// Test that contains0 |= contains0
 contains0 <- parse_core_mod "arrays" "contains0";
-mr_solver_debug 1 contains0 contains0;
+run_test "contains0 |= contains0" (mr_solver contains0 contains0) true;
diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index fd4ce458c2..5ad6828834 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -66,8 +66,6 @@ data MRFailure
   | MalformedDefsFun Term
   | MalformedComp Term
   | NotCompFunType Term
-  | CoIndHypMismatchWidened FunName FunName CoIndHyp
-  | CoIndHypMismatchFailure (NormComp, NormComp) (NormComp, NormComp)
     -- | A local variable binding
   | MRFailureLocalVar LocalName MRFailure
     -- | Information about the context of the failure
@@ -81,8 +79,8 @@ ppWithPrefix :: PrettyInCtx a => String -> a -> PPInCtxM SawDoc
 ppWithPrefix str a = (pretty str <>) <$> nest 2 <$> (line <>) <$> prettyInCtx a
 
 -- | Pretty-print two objects, prefixed with a 'String' and with a separator
-ppWithPrefixSep :: PrettyInCtx a => String -> a -> String -> a ->
-                   PPInCtxM SawDoc
+ppWithPrefixSep :: (PrettyInCtx a, PrettyInCtx b) =>
+                   String -> a -> String -> b -> PPInCtxM SawDoc
 ppWithPrefixSep d1 t2 d3 t4 =
   prettyInCtx t2 >>= \d2 -> prettyInCtx t4 >>= \d4 ->
   return $ group (pretty d1 <> nest 2 (line <> d2) <> line <>
@@ -124,13 +122,6 @@ instance PrettyInCtx MRFailure where
     ppWithPrefix "Could not handle computation:" t
   prettyInCtx (NotCompFunType tp) =
     ppWithPrefix "Not a computation or computational function type:" tp
-  prettyInCtx (CoIndHypMismatchWidened nm1 nm2 _) =
-    ppWithPrefixSep "[Internal] Trying to widen co-inductive hypothesis on:" nm1 "," nm2
-  prettyInCtx (CoIndHypMismatchFailure (tm1, tm2) (tm1', tm2')) =
-    do pp <- ppWithPrefixSep "" tm1 "|=" tm2
-       pp' <- ppWithPrefixSep "" tm1' "|=" tm2'
-       return $ "Could not match co-inductive hypothesis:" <> pp' <> line <>
-                                              "with goal:" <> pp
   prettyInCtx (MRFailureLocalVar x err) =
     local (x:) $ prettyInCtx err
   prettyInCtx (MRFailureCtx ctx err) =
@@ -184,16 +175,34 @@ data CoIndHyp = CoIndHyp {
   -- from outermost to innermost; that is, the uvars as "seen from outside their
   -- scope", which is the reverse of the order of 'mrUVars', below
   coIndHypCtx :: [(LocalName,Term)],
+  -- | The LHS function name
+  coIndHypLHSFun :: FunName,
+  -- | The RHS function name
+  coIndHypRHSFun :: FunName,
   -- | The LHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
   coIndHypLHS :: [Term],
   -- | The RHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
   coIndHypRHS :: [Term]
 } deriving Show
 
+-- | Extract the @i@th argument on either the left- or right-hand side of a
+-- coinductive hypothesis
+coIndHypArg :: CoIndHyp -> Either Int Int -> Term
+coIndHypArg (CoIndHyp _ _ _ args1 _) (Left i) = args1 !! i
+coIndHypArg (CoIndHyp _ _ _ _ args2) (Right i) = args2 !! i
+
 -- | A map from pairs of function names to co-inductive hypotheses over those
 -- names
 type CoIndHyps = Map (FunName, FunName) CoIndHyp
 
+instance PrettyInCtx CoIndHyp where
+  prettyInCtx (CoIndHyp ctx f1 f2 args1 args2) =
+    local (const $ map fst $ reverse ctx) $
+    prettyAppList [return (ppCtx ctx <> "."),
+                   prettyInCtx (FunBind f1 args1 CompFunReturn),
+                   return "|=",
+                   prettyInCtx (FunBind f2 args2 CompFunReturn)]
+
 -- | An assumption that a named function refines some specificaiton. This has
 -- the form
 --
@@ -244,14 +253,20 @@ data MRState = MRState {
   mrsVars :: MRVarMap
 }
 
+-- | The exception type for MR. Solver, which is either a 'MRFailure' or a
+-- widening request
+data MRExn = MRExnFailure MRFailure
+           | MRExnWiden FunName FunName [Either Int Int]
+           deriving Show
+
 -- | Mr. Monad, the monad used by MR. Solver, which has 'MRInfo' as as a
 -- shared environment, 'MRState' as state, and 'MRFailure' as an exception
 -- type, all over an 'IO' monad
 newtype MRM a = MRM { unMRM :: ReaderT MRInfo (StateT MRState
-                                              (ExceptT MRFailure IO)) a }
+                                              (ExceptT MRExn IO)) a }
               deriving (Functor, Applicative, Monad, MonadIO,
                         MonadReader MRInfo, MonadState MRState,
-                                            MonadError MRFailure)
+                                            MonadError MRExn)
 
 instance MonadTerm MRM where
   mkTermF = liftSC1 scTermF
@@ -301,23 +316,41 @@ runMRM sc timeout debug assumps m =
                               mriUVars = [], mriCoIndHyps = Map.empty,
                               mriAssumptions = true_tm }
      let init_st = MRState { mrsVars = Map.empty }
-     runExceptT $ flip evalStateT init_st $ flip runReaderT init_info $ unMRM m
+     res <- runExceptT $ flip evalStateT init_st $
+       flip runReaderT init_info $ unMRM m
+     case res of
+       Right a -> return $ Right a
+       Left (MRExnFailure failure) -> return $ Left failure
+       Left exn -> fail ("runMRM: unexpected internal exception: " ++ show exn)
+
+-- | Throw an 'MRFailure'
+throwMRFailure :: MRFailure -> MRM a
+throwMRFailure = throwError . MRExnFailure
 
 -- | Apply a function to any failure thrown by an 'MRM' computation
-mapFailure :: (MRFailure -> MRFailure) -> MRM a -> MRM a
-mapFailure f m = catchError m (throwError . f)
+mapMRFailure :: (MRFailure -> MRFailure) -> MRM a -> MRM a
+mapMRFailure f m = catchError m $ \case
+  MRExnFailure failure -> throwError $ MRExnFailure $ f failure
+  e -> throwError e
+
+-- | Catch any 'MRFailure' raised by a computation
+catchFailure :: MRM a -> (MRFailure -> MRM a) -> MRM a
+catchFailure m f =
+  m `catchError` \case
+  MRExnFailure failure -> f failure
+  e -> throwError e
 
 -- | Try two different 'MRM' computations, combining their failures if needed.
 -- Note that the 'MRState' will reset if the first computation fails.
 mrOr :: MRM a -> MRM a -> MRM a
 mrOr m1 m2 =
-  catchError m1 $ \err1 ->
-  catchError m2 $ \err2 ->
-  throwError $ MRFailureDisj err1 err2
+  catchFailure m1 $ \err1 ->
+  catchFailure m2 $ \err2 ->
+  throwMRFailure $ MRFailureDisj err1 err2
 
 -- | Run an 'MRM' computation in an extended failure context
 withFailureCtx :: FailCtx -> MRM a -> MRM a
-withFailureCtx ctx = mapFailure (MRFailureCtx ctx)
+withFailureCtx ctx = mapMRFailure (MRFailureCtx ctx)
 
 {-
 -- | Catch any errors thrown by a computation and coerce them to a 'Left'
@@ -394,11 +427,20 @@ mrApplyAll f args = liftSC2 scApplyAll f args >>= liftSC1 betaNormalize
 -- types as SAW core 'Term's, with the least recently bound uvar first, i.e., in
 -- the order as seen "from the outside"
 mrUVarCtx :: MRM [(LocalName,Term)]
-mrUVarCtx = reverse <$> map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars
+mrUVarCtx = reverse <$> mrUVarCtxRev
+
+-- | Get the current context of uvars as a list of variable names and their
+-- types as SAW core 'Term's, with the most recently bound uvar first, i.e., in
+-- the order as seen "from the inside"
+mrUVarCtxRev :: MRM [(LocalName,Term)]
+mrUVarCtxRev = map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars
 
 -- | Get the type of a 'Term' in the current uvar context
 mrTypeOf :: Term -> MRM Term
-mrTypeOf t = mrUVarCtx >>= \ctx -> liftSC2 scTypeOf' (map snd ctx) t
+mrTypeOf t =
+  -- NOTE: scTypeOf' wants the type context in the most recently bound var
+  -- first, i.e., in the mrUVarCtxRev order
+  mrUVarCtxRev >>= \ctx -> liftSC2 scTypeOf' (map snd ctx) t
 
 -- | Check if two 'Term's are convertible in the 'MRM' monad
 mrConvertible :: Term -> Term -> MRM Bool
@@ -419,7 +461,7 @@ mrFunOutType fname args =
        debugPrint 0 ("Expected: " ++ show (length vars) ++
                      ", found: " ++ show (length args))
        debugPretty 0 ("For function: " <> pp_fname <> " with type: " <> pp_ftype)
-       error"mrFunOutType"
+       error "mrFunOutType"
 
 -- | Turn a 'LocalName' into one not in a list, adding a suffix if necessary
 uniquifyName :: LocalName -> [LocalName] -> LocalName
@@ -430,16 +472,19 @@ uniquifyName nm nms =
     Just nm' -> nm'
     Nothing -> error "uniquifyName"
 
+-- | Turn a list of 'LocalName's into one names not in a list, adding suffixes
+-- if necessary
+uniquifyNames :: [LocalName] -> [LocalName] -> [LocalName]
+uniquifyNames [] _ = []
+uniquifyNames (nm:nms) nms_other =
+  let nm' = uniquifyName nm nms_other in
+  nm' : uniquifyNames nms (nm' : nms_other)
+
 -- | Run a MR Solver computation in a context extended with a universal
 -- variable, which is passed as a 'Term' to the sub-computation. Note that any
 -- assumptions made in the sub-computation will be lost when it completes.
 withUVar :: LocalName -> Type -> (Term -> MRM a) -> MRM a
-withUVar nm tp m =
-  do nm' <- uniquifyName nm <$> map fst <$> mrUVars
-     assumps' <- mrAssumptions >>= liftTerm 0 1
-     local (\info -> info { mriUVars = (nm',tp) : mriUVars info,
-                            mriAssumptions = assumps' }) $
-       mapFailure (MRFailureLocalVar nm') (liftSC1 scLocalVar 0 >>= m)
+withUVar nm (Type tp) m = withUVars [(nm,tp)] (\[v] -> m v)
 
 -- | Run a MR Solver computation in a context extended with a universal variable
 -- and pass it the lifting (in the sense of 'incVars') of an MR Solver term
@@ -453,16 +498,25 @@ withUVarLift nm tp t m =
 -- The variables are bound "outside in", meaning the first variable in the list
 -- is bound outermost, and so will have the highest deBruijn index.
 withUVars :: [(LocalName,Term)] -> ([Term] -> MRM a) -> MRM a
-withUVars = helper [] where
-  -- The extra input list gives the variables that have already been bound, in
-  -- order from most to least recently bound
-  helper :: [Term] -> [(LocalName,Term)] -> ([Term] -> MRM a) -> MRM a
-  helper vars [] m = m $ reverse vars
-  helper vars ((nm,tp):ctx) m =
-    -- FIXME: I think substituting here is wrong, but works on closed terms, so
-    -- it's fine to use at the top level at least...
-    substTerm 0 vars tp >>= \tp' ->
-    withUVarLift nm (Type tp') vars $ \var vars' -> helper (var:vars') ctx m
+withUVars [] f = f []
+withUVars ctx f =
+  do nms <- uniquifyNames (map fst ctx) <$> map fst <$> mrUVars
+     let ctx_u = zip nms $ map (Type . snd) ctx
+     assumps' <- mrAssumptions >>= liftTerm 0 (length ctx)
+     vars <- reverse <$> mapM (liftSC1 scLocalVar) [0 .. length ctx - 1]
+     local (\info -> info { mriUVars = reverse ctx_u ++ mriUVars info,
+                            mriAssumptions = assumps' }) $
+       foldr (\nm m -> mapMRFailure (MRFailureLocalVar nm) m) (f vars) nms
+
+-- | Run a MR Solver in a top-level context, i.e., with no uvars or assumptions
+withNoUVars :: MRM a -> MRM a
+withNoUVars m =
+  do true_tm <- liftSC1 scBool True
+     local (\info -> info { mriUVars = [], mriAssumptions = true_tm }) m
+
+-- | Run a MR Solver in a context of only the specified UVars, no others
+withOnlyUVars :: [(LocalName,Term)] -> MRM a -> MRM a
+withOnlyUVars vars m = withNoUVars $ withUVars vars $ const m
 
 -- | Build 'Term's for all the uvars currently in scope, ordered from least to
 -- most recently bound
@@ -699,32 +753,13 @@ _mrSubstEVarsStrict = mrSubstEVarsStrict
 mrGetCoIndHyp :: FunName -> FunName -> MRM (Maybe CoIndHyp)
 mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps
 
--- | Run a compuation under the additional co-inductive assumption that
--- @forall x1, ..., xn. F y1 ... ym |= G z1 ... zl@, where @F@ and @G@ are
--- the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@ are the given
--- argument lists, and @x1, ..., xn@ is the current context of uvars. If
--- while running the given computation a 'CoIndHypMismatchWidened' error is
--- reached with the given names, the state is restored and the computation is
--- re-run with the widened hypothesis. This is done recursively, meaning this
--- function will only return once no 'CoIndHypMismatchWidened' errors are
--- raised with the given names.
-withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a
-withCoIndHyp nm1 args1 nm2 args2 m =
-  do ctx <- mrUVarCtx
-     withCoIndHyp' (nm1, nm2) (CoIndHyp ctx args1 args2) m
-
--- | The main loop of 'withCoIndHyp'
-withCoIndHyp' :: (FunName, FunName) -> CoIndHyp -> MRM a -> MRM a
-withCoIndHyp' (nm1, nm2) hyp@(CoIndHyp _ args1 args2) m =
-  do mrDebugPPPrefixSep 1 "withCoIndHyp" (FunBind nm1 args1 CompFunReturn)
-                                    "|=" (FunBind nm2 args2 CompFunReturn)
-     st <- get
-     hyps' <- Map.insert (nm1, nm2) hyp <$> mrCoIndHyps
-     (local (\info -> info { mriCoIndHyps = hyps' }) m) `catchError` \case
-       CoIndHypMismatchWidened nm1' nm2' hyp' | nm1 == nm1' && nm2 == nm2'
-         -> -- FIXME: Could restoring the state here cause any problems?
-            put st >> withCoIndHyp' (nm1, nm2) hyp' m
-       e -> throwError e
+-- | Run a compuation under an additional co-inductive assumption
+withCoIndHypRaw :: CoIndHyp -> MRM a -> MRM a
+withCoIndHypRaw hyp m =
+  do debugPretty 1 ("withCoIndHyp" <+> ppInEmptyCtx hyp)
+     hyps' <- Map.insert (coIndHypLHSFun hyp,
+                          coIndHypRHSFun hyp) hyp <$> mrCoIndHyps
+     local (\info -> info { mriCoIndHyps = hyps' }) m
 
 -- | Generate fresh evars for the context of a 'CoIndHyp' and
 -- substitute them into its arguments and right-hand side
@@ -791,8 +826,8 @@ mrPPInCtx a =
 
 -- | Pretty-print the result of 'ppWithPrefixSep' relative to the current uvar
 -- context to 'stderr' if the debug level is at least the 'Int' provided
-mrDebugPPPrefixSep :: PrettyInCtx a => Int -> String -> a -> String -> a ->
-                      MRM ()
+mrDebugPPPrefixSep :: (PrettyInCtx a, PrettyInCtx b) =>
+                      Int -> String -> a -> String -> b -> MRM ()
 mrDebugPPPrefixSep i pre a1 sp a2 =
   mrUVars >>= \ctx ->
   debugPretty i $
diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index f597b35756..7043c9f565 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -177,6 +177,7 @@ mrProvableRaw prop_term =
 -- | Test if a Boolean term over the current uvars is provable given the current
 -- assumptions
 mrProvable :: Term -> MRM Bool
+mrProvable (asBool -> Just b) = return b
 mrProvable bool_tm =
   do assumps <- mrAssumptions
      prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue
@@ -276,12 +277,10 @@ mrAssertProveEq :: Term -> Term -> MRM ()
 mrAssertProveEq t1 t2 =
   do success <- mrProveEq t1 t2
      if success then return () else
-       throwError (TermsNotEq t1 t2)
+       throwMRFailure (TermsNotEq t1 t2)
 
--- | The main workhorse for 'prProveEq'. Build a Boolean term expressing that
--- the third and fourth arguments, whose type is given by the second. This is
--- done in a continuation monad so that the output term can be in a context with
--- additional universal variables.
+-- | The main workhorse for 'mrProveEq'. Build a Boolean term expressing that
+-- the third and fourth arguments, whose type is given by the second.
 mrProveEqH :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM TermInCtx
 
 {-
@@ -309,6 +308,10 @@ mrProveEqH var_map _tp t1 (asEVarApp var_map -> Just (evar, args, Nothing)) =
      success <- mrTrySetAppliedEVar evar args t1'
      TermInCtx [] <$> liftSC1 scBool success
 
+-- For unit types, always return true
+mrProveEqH _ (asTupleType -> Just []) _ _ =
+  TermInCtx [] <$> liftSC1 scBool True
+
 -- For the nat, bitvector, Boolean, and integer types, call mrProveEqSimple
 mrProveEqH _ (asDataType -> Just (pn, [])) t1 t2
   | primName pn == "Prelude.Nat" =
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 49452fe4d6..84b4a2febb 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -114,6 +114,8 @@ C |- F e1 ... en >>= k |= F' e1' ... em' >>= k':
 
 module SAWScript.Prover.MRSolver.Solver where
 
+import Data.Either
+import Data.List (findIndices)
 import Control.Monad.Except
 import qualified Data.Map as Map
 
@@ -139,7 +141,7 @@ asLRTList (asCtor -> Just (primName -> "Prelude.LRT_Cons", [lrt, lrts])) =
   do tp <- liftSC2 scGlobalApply "Prelude.lrtToType" [lrt]
      tp_norm_closed <- liftSC1 scWhnf tp >>= piUVarsM
      (tp_norm_closed :) <$> asLRTList lrts
-asLRTList t = throwError (MalformedLetRecTypes t)
+asLRTList t = throwMRFailure (MalformedLetRecTypes t)
 
 -- | Match a right-nested series of pairs. This is similar to 'asTupleValue'
 -- except that it expects a unit value to always be at the end.
@@ -179,7 +181,7 @@ mrFreshLetRecVars lrts defs_f =
     defs_tm <- mrApplyAll defs_f fun_tms
     defs <- case asNestedPairs defs_tm of
       Just defs -> return defs
-      Nothing -> throwError (MalformedDefsFun defs_f)
+      Nothing -> throwMRFailure (MalformedDefsFun defs_f)
 
     -- Remember the body associated with each fresh function constant
     zipWithM_ (\f body ->
@@ -269,7 +271,7 @@ normComp (CompTerm t) =
     ((asGlobalFunName -> Just f), args) ->
       return $ FunBind f args CompFunReturn
 
-    _ -> throwError (MalformedComp t)
+    _ -> throwMRFailure (MalformedComp t)
 
 
 -- | Bind a computation in whnf with a function, and normalize
@@ -314,16 +316,16 @@ applyNormCompFun f arg = applyCompFun f arg >>= normComp
 -- not allowed, either because it is a global function we are treating as opaque
 -- or because it is a locally-bound function variable
 mrLookupFunDef :: FunName -> MRM Term
-mrLookupFunDef f@(GlobalName _) = throwError (CannotLookupFunDef f)
+mrLookupFunDef f@(GlobalName _) = throwMRFailure (CannotLookupFunDef f)
 mrLookupFunDef f@(LocalName var) =
   mrVarInfo var >>= \case
   Just (FunVarInfo body) -> return body
-  Just _ -> throwError (CannotLookupFunDef f)
+  Just _ -> throwMRFailure (CannotLookupFunDef f)
   Nothing -> error "mrLookupFunDef: unknown variable!"
 
 -- | Unfold a call to function @f@ in term @f args >>= g@
 mrUnfoldFunBind :: FunName -> [Term] -> Mark -> CompFun -> MRM Comp
-mrUnfoldFunBind f _ mark _ | inMark f mark = throwError (RecursiveUnfold f)
+mrUnfoldFunBind f _ mark _ | inMark f mark = throwMRFailure (RecursiveUnfold f)
 mrUnfoldFunBind f args mark g =
   do f_def <- mrLookupFunDef f
      CompBind <$>
@@ -339,6 +341,88 @@ handling the recursive ones
 -}
 
 
+----------------------------------------------------------------------
+-- * Handling Coinductive Hypotheses
+----------------------------------------------------------------------
+
+-- | Run a compuation under the additional co-inductive assumption that
+-- @forall x1, ..., xn. F y1 ... ym |= G z1 ... zl@, where @F@ and @G@ are
+-- the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@ are the given
+-- argument lists, and @x1, ..., xn@ is the current context of uvars. If
+-- while running the given computation a 'CoIndHypMismatchWidened' error is
+-- reached with the given names, the state is restored and the computation is
+-- re-run with the widened hypothesis.
+withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a
+withCoIndHyp f1 args1 f2 args2 m =
+  do ctx <- mrUVarCtx
+     withCoIndHyp' (CoIndHyp ctx f1 f2 args1 args2) m
+
+-- | The main loop of 'withCoIndHyp'
+withCoIndHyp' :: CoIndHyp -> MRM a -> MRM a
+withCoIndHyp' hyp m =
+  withCoIndHypRaw hyp m `catchError` \case
+  MRExnWiden nm1' nm2' new_vars
+    | coIndHypLHSFun hyp == nm1' && coIndHypRHSFun hyp == nm2' ->
+        -- NOTE: the state automatically gets reset here because we defined MRM
+        -- with ExceptT at a lower level than StateT
+        do mrDebugPPPrefixSep 1 "Widening recursive assumption for" nm1' "|=" nm2'
+           hyp' <- generalizeCoIndHyp hyp new_vars
+           withCoIndHyp' hyp' m
+  e -> throwError e
+
+
+-- | Test that a coinductive hypothesis for the given function names matches the
+-- given arguments, otherwise throw an exception saying that widening is needed
+matchCoIndHyp :: CoIndHyp -> [Term] -> [Term] -> MRM ()
+matchCoIndHyp hyp args1 args2 =
+  do (args1', args2') <- instantiateCoIndHyp hyp
+     eqs1 <- zipWithM mrProveEq args1' args1
+     eqs2 <- zipWithM mrProveEq args2' args2
+     if and (eqs1 ++ eqs2) then return () else
+       throwError $ MRExnWiden (coIndHypLHSFun hyp) (coIndHypRHSFun hyp)
+       (map Left (findIndices not eqs1) ++ map Right (findIndices not eqs1))
+
+-- | Generalize some of the arguments of a coinductive hypothesis
+generalizeCoIndHyp :: CoIndHyp -> [Either Int Int] -> MRM CoIndHyp
+generalizeCoIndHyp hyp [] = return hyp
+generalizeCoIndHyp hyp all_specs@(arg_spec:arg_specs) =
+  withOnlyUVars (coIndHypCtx hyp) $ do
+  mrDebugPPPrefixSep 2 "generalizeCoIndHyp" hyp "with arg specs" (show all_specs)
+  -- Get the arg and type associated with arg_spec
+  let arg = coIndHypArg hyp arg_spec
+  arg_tp <- mrTypeOf arg
+  ctx <- mrUVarCtx
+  debugPretty 2 ("Current context: " <> ppCtx ctx)
+  -- Sort out the other args that equal arg
+  eq_uneq_specs <- forM arg_specs $ \spec' ->
+    do let arg' = coIndHypArg hyp spec'
+       tp' <- mrTypeOf arg'
+       mrDebugPPPrefixSep 2 "generalizeCoIndHyp: the type of" arg' "is" tp'
+       debugPrint 2 ("arg' = " ++ show arg')
+       tps_eq <- mrConvertible arg_tp tp'
+       args_eq <- if tps_eq then mrProveEq arg arg' else return False
+       return $ if args_eq then Left spec' else Right spec'
+  let (eq_specs, uneq_specs) = partitionEithers eq_uneq_specs
+  -- Add a new variable of type arg_tp, set all eq_specs plus our original
+  -- arg_spec to it, and recurse
+  hyp' <- generalizeCoIndHypArgs hyp arg_tp (arg_spec:eq_specs)
+  generalizeCoIndHyp hyp' uneq_specs
+
+-- | Add a new variable of the given type to the context of a coinductive
+-- hypothesis and set the specified arguments to that new variable
+generalizeCoIndHypArgs :: CoIndHyp -> Term -> [Either Int Int] -> MRM CoIndHyp
+generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2) tp specs =
+  do let set_arg i args =
+           take i args ++ (Unshared $ LocalVar 0) : drop (i+1) args
+     let (specs1, specs2) = partitionEithers specs
+     -- NOTE: need to lift the arguments because we are adding a variable
+     args1' <- liftTermLike 0 1 args1
+     args2' <- liftTermLike 0 1 args2
+     let args1'' = foldr set_arg args1' specs1
+         args2'' = foldr set_arg args2' specs2
+     return $ CoIndHyp (ctx ++ [("z",tp)]) f1 f2 args1'' args2''
+
+
 ----------------------------------------------------------------------
 -- * Mr Solver Himself (He Identifies as Male)
 ----------------------------------------------------------------------
@@ -367,8 +451,8 @@ mrRefines t1 t2 =
 mrRefines' :: NormComp -> NormComp -> MRM ()
 mrRefines' (ReturnM e1) (ReturnM e2) = mrAssertProveEq e1 e2
 mrRefines' (ErrorM _) (ErrorM _) = return ()
-mrRefines' (ReturnM e) (ErrorM _) = throwError (ReturnNotError e)
-mrRefines' (ErrorM _) (ReturnM e) = throwError (ReturnNotError e)
+mrRefines' (ReturnM e) (ErrorM _) = throwMRFailure (ReturnNotError e)
+mrRefines' (ErrorM _) (ReturnM e) = throwMRFailure (ReturnNotError e)
 mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 =
   do cond <- mrEq' tp e1 e2
      not_cond <- liftSC1 scNot cond
@@ -430,9 +514,9 @@ mrRefines' (OrM m1 m1') m2 =
 -- FIXME: the following cases don't work unless we either allow evars to be set
 -- to NormComps or we can turn NormComps back into terms
 mrRefines' m1@(FunBind (EVarFunName _) _ _) m2 =
-  throwError (CompsDoNotRefine m1 m2)
+  throwMRFailure (CompsDoNotRefine m1 m2)
 mrRefines' m1 m2@(FunBind (EVarFunName _) _ _) =
-  throwError (CompsDoNotRefine m1 m2)
+  throwMRFailure (CompsDoNotRefine m1 m2)
 {-
 mrRefines' (FunBind (EVarFunName evar) args CompFunReturn) m2 =
   mrGetEVar evar >>= \case
@@ -464,14 +548,8 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   --   'CoIndHypMismatchWidened' error for 'withCoIndHyp' to catch)
   -- * Otherwise, throw a 'CoIndHypMismatchFailure' error.
   (Just hyp, _) ->
-    do (args1', args2') <- instantiateCoIndHyp hyp
-       mrWidenCoIndHyp f1 f2 args1 args2 args1' args2' >>= \case
-         Convertible -> mrRefinesFun k1 k2
-         Widened hyp' -> throwError (CoIndHypMismatchWidened f1 f2 hyp')
-         CouldNotWiden ->
-           let m1' = FunBind f1 args1' CompFunReturn
-               m2' = FunBind f2 args2' CompFunReturn
-            in throwError (CoIndHypMismatchFailure (m1, m2) (m1', m2'))
+    matchCoIndHyp hyp args1 args2 >>
+    mrRefinesFun k1 k2
 
   -- If we have an assumption that f1 args' refines some rhs, then prove that
   -- args1 = args' and then that rhs refines m2
@@ -506,7 +584,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   -- continuation on the other side, but we don't know how to do that, so give
   -- up
   _ ->
-    throwError (CompsDoNotRefine m1 m2)
+    throwMRFailure (CompsDoNotRefine m1 m2)
 
 {- FIXME: handle FunBind on just one side
 mrRefines' m1@(FunBind f@(GlobalName _) args k1) m2 =
@@ -521,7 +599,7 @@ mrRefines' m1@(FunBind f@(GlobalName _) args k1) m2 =
   Nothing ->
     -- We don't want to do inter-procedural proofs, so if we don't know anything
     -- about f already then give up
-    throwError (CompsDoNotRefine m1 m2)
+    throwMRFailure (CompsDoNotRefine m1 m2)
 -}
 
 
@@ -548,7 +626,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2 =
     -- form m2' >>= k2 where f1 args1 |= m2' and k1 |= k2, but we don't know how
     -- to do this splitting, so give up
     _ ->
-      throwError (CompsDoNotRefine m1 m2)
+      throwMRFailure (CompsDoNotRefine m1 m2)
 
 
 mrRefines' m1 m2@(FunBind f2 args2 k2) =
@@ -571,7 +649,7 @@ mrRefines' m1 m2@(FunBind f2 args2 k2) =
     -- form m1' >>= k1 where m1' |= f2 args2 and k1 |= k2, but we don't know how
     -- to do this splitting, so give up
   _ ->
-    throwError (CompsDoNotRefine m1 m2)
+    throwMRFailure (CompsDoNotRefine m1 m2)
 
 
 -- NOTE: the rules that introduce existential variables need to go last, so that
@@ -588,7 +666,7 @@ mrRefines' (ForallM tp f1) m2 =
      mrRefines m1' m2
 
 -- If none of the above cases match, then fail
-mrRefines' m1 m2 = throwError (CompsDoNotRefine m1 m2)
+mrRefines' m1 m2 = throwMRFailure (CompsDoNotRefine m1 m2)
 
 
 -- | Prove that one function refines another for all inputs
@@ -604,26 +682,6 @@ mrRefinesFun f1 f2
 mrRefinesFun _ _ = error "mrRefinesFun: unreachable!"
 
 
--- | The result type of 'mrWidenCoIndHyp'
-data WidenCoIndHypResult = Convertible | Widened CoIndHyp | CouldNotWiden
-
--- | Given a goal and a co-inductive hypothesis over the same pair of function
--- names, try to widen them into a more general co-inductive hypothesis which
--- implies both the given goal and the given co-inductive hypothesis. Returns
--- 'Convertible' if the goal and co-inductive hypothesis are convertible (and
--- therefore no widening needs to be done), 'Widened' if widening was
--- successful, and 'CouldNotWiden' if the terms are neither convertible nor
--- able to be widened.
--- FIXME: Finish implementing this function!
-mrWidenCoIndHyp :: FunName -> FunName ->
-                    [Term] -> [Term] -> [Term] -> [Term] ->
-                    MRM WidenCoIndHypResult
-mrWidenCoIndHyp _f1 _f2 args1 args2 args1' args2' =
-  do eq1 <- and <$> zipWithM mrProveEq args1' args1
-     eq2 <- and <$> zipWithM mrProveEq args2' args2
-     return $ if eq1 && eq2 then Convertible else CouldNotWiden
-
-
 ----------------------------------------------------------------------
 -- * External Entrypoints
 ----------------------------------------------------------------------
@@ -645,7 +703,7 @@ askMRSolver sc dlvl timeout t1 t2 =
          withUVars uvar_ctx $ \vars ->
          do tps_are_eq <- mrConvertible tp1 tp2
             if tps_are_eq then return () else
-              throwError (TypesNotEq (Type tp1) (Type tp2))
+              throwMRFailure (TypesNotEq (Type tp1) (Type tp2))
             mrDebugPPPrefixSep 1 "mr_solver" t1 "|=" t2
             m1 <- mrApplyAll t1 vars >>= normCompTerm
             m2 <- mrApplyAll t2 vars >>= normCompTerm
diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs
index 4c8dd86991..21669abb60 100644
--- a/src/SAWScript/Prover/MRSolver/Term.hs
+++ b/src/SAWScript/Prover/MRSolver/Term.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 {- |
 Module      : SAWScript.Prover.MRSolver.Term
@@ -18,6 +20,7 @@ normalization - see @Solver.hs@ for the description of this normalization.
 
 module SAWScript.Prover.MRSolver.Term where
 
+import Data.String
 import Data.IORef
 import Control.Monad.Reader
 import qualified Data.IntMap as IntMap
@@ -264,6 +267,10 @@ showInCtx :: PrettyInCtx a => [LocalName] -> a -> String
 showInCtx ctx a =
   renderSawDoc defaultPPOpts $ runReader (prettyInCtx a) ctx
 
+-- | Pretty-print an object in the empty SAW core context
+ppInEmptyCtx :: PrettyInCtx a => a -> SawDoc
+ppInEmptyCtx a = runReader (prettyInCtx a) []
+
 -- | A generic function for pretty-printing an object in a SAW core context of
 -- locally-bound names
 class PrettyInCtx a where
@@ -276,6 +283,22 @@ instance PrettyInCtx Term where
 prettyAppList :: [PPInCtxM SawDoc] -> PPInCtxM SawDoc
 prettyAppList = fmap (group . hang 2 . vsep) . sequence
 
+-- | FIXME: move this helper function somewhere better...
+ppCtx :: [(LocalName,Term)] -> SawDoc
+ppCtx = helper [] where
+  helper :: [LocalName] -> [(LocalName,Term)] -> SawDoc
+  helper _ [] = ""
+  helper ns ((n,tp):ctx) =
+    let ns' = n:ns in
+    ppTermInCtx defaultPPOpts ns' (Unshared $ LocalVar 0) <> ":" <>
+    ppTermInCtx defaultPPOpts ns tp <> ", " <> helper ns' ctx
+
+instance PrettyInCtx String where
+  prettyInCtx str = return $ fromString str
+
+instance PrettyInCtx SawDoc where
+  prettyInCtx pp = return pp
+
 instance PrettyInCtx Type where
   prettyInCtx (Type t) = prettyInCtx t