diff --git a/hermit.cabal b/hermit.cabal
--- a/hermit.cabal
+++ b/hermit.cabal
@@ -1,5 +1,5 @@
 Name:                hermit
-Version:             0.7.0.0
+Version:             0.7.1.0
 Synopsis:            Haskell Equational Reasoning Model-to-Implementation Tunnel
 Description:
   HERMIT is a Haskell-specific toolkit designed to mechanize
@@ -15,12 +15,12 @@
   .
   @
    $ hermit Reverse.hs Reverse.hss resume
-   [starting HERMIT v0.7.0.0 on Reverse.hs]
+   [starting HERMIT v0.7.1.0 on Reverse.hs]
    % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:Main:Reverse.hss -fplugin-opt=HERMIT:Main:resume
    [1 of 2] Compiling HList            ( HList.hs, HList.o )
    Loading package ghc-prim ... linking ... done.
    ...
-   Loading package hermit-0.7.0.0 ... linking ... done.
+   Loading package hermit-0.7.1.0 ... linking ... done.
    [2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )
    Linking Reverse ...
    $ ./Reverse
@@ -31,12 +31,12 @@
   .
   @
    $ hermit Reverse.hs
-   [starting HERMIT v0.7.0.0 on Reverse.hs]
+   [starting HERMIT v0.7.1.0 on Reverse.hs]
    % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:*:
    [1 of 2] Compiling HList            ( HList.hs, HList.o )
    Loading package ghc-prim ... linking ... done.
    ...
-   Loading package hermit-0.7.0.0 ... linking ... done.
+   Loading package hermit-0.7.1.0 ... linking ... done.
    [2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )
    ===================== Welcome to HERMIT =====================
    HERMIT is a toolkit for the interactive transformation of GHC
diff --git a/src/HERMIT/Dictionary/GHC.hs b/src/HERMIT/Dictionary/GHC.hs
--- a/src/HERMIT/Dictionary/GHC.hs
+++ b/src/HERMIT/Dictionary/GHC.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE CPP, FlexibleContexts #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
 module HERMIT.Dictionary.GHC
     ( -- * GHC-based Transformations
       -- | This module contains transformations that are reflections of GHC functions, or derived from GHC functions.
@@ -15,6 +17,8 @@
       -- A zombie is an identifer that has 'OccInfo' 'IAmDead', but still has occurrences.
     , lintExprT
     , lintModuleT
+    , lintQuantifiedT
+    , lintClauseT
     , occurAnalyseR
     , occurAnalyseChangedR
     , occurAnalyseExprChangedR
@@ -29,9 +33,11 @@
 import qualified CoreLint
 
 import           Control.Arrow
+import           Control.Monad
 import           Control.Monad.IO.Class
 
 import           Data.Char (isSpace)
+import           Data.Either (partitionEithers)
 import           Data.List (mapAccumL)
 import qualified Data.Map as M
 import           Data.String
@@ -64,8 +70,12 @@
         , "will catch that however."] .+ Deep .+ Debug .+ Query
     , external "lint-module" (promoteModGutsT lintModuleT :: TransformH LCoreTC String)
         [ "Runs GHC's Core Lint, which typechecks the current module."] .+ Deep .+ Debug .+ Query
-    , external "load-lemma-library" (loadLemmaLibraryT :: HermitName -> TransformH LCore ())
+    , external "lint" (promoteT lintQuantifiedT :: TransformH LCoreTC String)
+        [ "Lint check a quantified clause." ]
+    , external "load-lemma-library" (flip loadLemmaLibraryT Nothing :: HermitName -> TransformH LCore String)
         [ "Dynamically load a library of lemmas." ]
+    , external "load-lemma-library" ((\nm -> loadLemmaLibraryT nm . Just) :: HermitName -> LemmaName -> TransformH LCore String)
+        [ "Dynamically load a specific lemma from a library of lemmas." ]
     ]
 
 ------------------------------------------------------------------------
@@ -180,16 +190,6 @@
 occurrenceAnalysisR :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, HasEmptyContext c, MonadCatch m, Walker c LCore) => Rewrite c m LCore
 occurrenceAnalysisR = occurAnalyseAndDezombifyR
 
-{- Does not work (no export)
--- Here is a hook into the occur analysis, and a way of looking at the result
-occAnalysis ::  CoreExpr -> UsageDetails
-occAnalysis = fst . occAnal (initOccEnv all_active_rules)
-
-lookupUsageDetails :: UsageDetails -> Var -> Maybe OccInfo
-lookupUsageDetails = lookupVarEnv
-
--}
-
 ----------------------------------------------------------------------
 
 -- TODO: this is mostly an example, move somewhere?
@@ -227,19 +227,52 @@
                 [NonRec v e] | i == v -> e -- the common case that we would have gotten a single non-recursive let
                 _ -> mkCoreLets bnds (varToCoreExpr i)
 
+----------------------------------------------------------------------
+
+lintQuantifiedT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)
+                => Transform c m Quantified String
+lintQuantifiedT = lintQuantifiedWorkT []
+
+lintQuantifiedWorkT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)
+                    => [Var] -> Transform c m Quantified String
+lintQuantifiedWorkT bs = readerT $ \ (Quantified bs' _) -> quantifiedT successT (lintClauseT (bs++bs')) (flip const)
+
+lintClauseT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)
+            => [Var] -> Transform c m Clause String
+lintClauseT bs = do
+    t <- readerT $ \case Equiv {} -> return $ promoteT ({- arr (mkCoreLams bs) >>> -} lintExprT) -- TODO: why does this break core lint?!
+                         _        -> return $ promoteT (lintQuantifiedWorkT bs)
+    (w1,w2) <- clauseT t t (const (,))
+    return $ unlines [w1,w2]
+
+----------------------------------------------------------------------
+
 -- | A LemmaLibrary is a transformation that produces a set of lemmas,
 -- which are then added to the lemma store. It is not allowed to insert
 -- its own lemmas directly (if it tries they are throw away), but can
 -- certainly read the existing store.
 type LemmaLibrary = TransformH () Lemmas
 
-loadLemmaLibraryT :: HermitName -> TransformH x ()
-loadLemmaLibraryT nm = contextonlyT $ \ c -> do
-    hscEnv <- getHscEnv
-    comp <- liftAndCatchIO $ loadLemmaLibrary hscEnv nm
-    m' <- applyT comp c () -- TODO: discard side effects
-    m <- getLemmas
-    putLemmas $ m' `M.union` m
+loadLemmaLibraryT :: HermitName -> Maybe LemmaName -> TransformH x String
+loadLemmaLibraryT nm mblnm = prefixFailMsg "Loading lemma library failed: " $
+    contextonlyT $ \ c -> do
+        hscEnv <- getHscEnv
+        comp <- liftAndCatchIO $ loadLemmaLibrary hscEnv nm
+        ls <- applyT comp c () -- TODO: discard side effects
+        nls <- maybe (return $ M.toList ls)
+                     (\lnm -> maybe (fail $ show lnm ++ " not found in library.")
+                                    (\ l -> return [(lnm,l)])
+                                    (M.lookup lnm ls))
+                     mblnm
+        r <- forM nls $ \ nl@(n, l) -> do
+                    er <- attemptM $ applyT lintQuantifiedT c $ lemmaQ l
+                    case er of
+                        Left msg -> return $ Left $ "Not adding lemma " ++ show n ++ " because lint failed.\n" ++ msg
+                        Right _  -> return $ Right nl
+        let (fs,nls') = partitionEithers r
+        m <- getLemmas
+        putLemmas $ (M.fromList nls') `M.union` m
+        return $ unlines (fs ++ ["Successfully loaded library " ++ show nm])
 
 loadLemmaLibrary :: HscEnv -> HermitName -> IO LemmaLibrary
 loadLemmaLibrary hscEnv hnm = do
diff --git a/src/HERMIT/Dictionary/Local/Case.hs b/src/HERMIT/Dictionary/Local/Case.hs
--- a/src/HERMIT/Dictionary/Local/Case.hs
+++ b/src/HERMIT/Dictionary/Local/Case.hs
@@ -226,7 +226,7 @@
             appAllR idR (caseAllR idR idR idR (\ n -> let vs = varSetElems (altCaptures !! n)
                                                       in if null vs then idR else alphaAltVarsR vs
                                               )
-                        ) >>> caseFloatArgR Nothing Nothing
+                        ) >>> caseFloatArgLemmaR u nm
 
 -- | case (case s1 of alt11 -> e11; alt12 -> e12) of alt21 -> e21; alt22 -> e22
 --   ==>
diff --git a/src/HERMIT/Dictionary/Reasoning.hs b/src/HERMIT/Dictionary/Reasoning.hs
--- a/src/HERMIT/Dictionary/Reasoning.hs
+++ b/src/HERMIT/Dictionary/Reasoning.hs
@@ -25,8 +25,7 @@
     , lemmaBiR
     , lemmaConsequentR
     , markLemmaUsedT
-    , markLemmaProvedT
-    , markLemmaAssumedT
+    , markLemmaProvenT
     , modifyLemmaT
     , showLemmaT
     , showLemmasT
@@ -40,11 +39,9 @@
     , lhsR
     , rhsR
     , bothR
-    , forallVarsT
     , verifyQuantifiedT
     , verifyEquivalentT
     , verifyOrCreateT
-    , lintQuantifiedT
     , verifyEqualityLeftToRightT
     , verifyEqualityCommonTargetT
     , verifyIsomorphismT
@@ -119,8 +116,6 @@
         [ "disjunt new-name lhs-name rhs-name" ]
     , external "imply" (\n1 n2 n3 -> implyLemmasT n1 n2 n3 :: TransformH LCore ())
         [ "imply new-name antecedent-name consequent-name" ]
-    , external "lint" (promoteT lintQuantifiedT :: TransformH LCoreTC String)
-        [ "Lint check a quantified clause." ]
     , external "lemma-birewrite" (promoteExprBiR . lemmaBiR Obligation :: LemmaName -> BiRewriteH LCore)
         [ "Generate a bi-directional rewrite from a lemma." ]
     , external "lemma-forward" (forwardT . promoteExprBiR . lemmaBiR Obligation :: LemmaName -> RewriteH LCore)
@@ -261,27 +256,6 @@
 
 ------------------------------------------------------------------------------
 
--- | Original clause passed to function so it can decide how to handle connective.
-clauseT :: (Monad m, ExtendPath c Crumb) => Transform c m LCore a -> Transform c m LCore b -> (Clause -> a -> b -> d) -> Transform c m Clause d
-clauseT t1 t2 f = readerT $ \ cl -> case cl of
-                                      Conj{}  -> conjT  (extractT t1) (extractT t2) (f cl)
-                                      Disj{}  -> disjT  (extractT t1) (extractT t2) (f cl)
-                                      Impl{}  -> implT  (extractT t1) (extractT t2) (f cl)
-                                      Equiv{} -> equivT (extractT t1) (extractT t2) (f cl)
-
-clauseR :: (Monad m, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m LCore -> Rewrite c m Clause
-clauseR r1 r2 = readerT $ \case
-                             Conj{}  -> conjAllR (extractR r1) (extractR r2)
-                             Disj{}  -> disjAllR (extractR r1) (extractR r2)
-                             Impl{}  -> implAllR (extractR r1) (extractR r2)
-                             Equiv{} -> equivAllR (extractR r1) (extractR r2)
-
--- | Lift a transformation over '[Var]' into a transformation over the universally quantified variables of a 'Quantified'.
-forallVarsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m [Var] b -> Transform c m Quantified b
-forallVarsT t = quantifiedT t successT const
-
-------------------------------------------------------------------------------
-
 showLemmasT :: Maybe LemmaName -> PrettyPrinter -> PrettyH a
 showLemmasT mnm pp = do
     ls <- getLemmasT
@@ -350,24 +324,6 @@
 
 ------------------------------------------------------------------------------
 
-lintQuantifiedT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)
-                => Transform c m Quantified String
-lintQuantifiedT = lintQuantifiedWorkT []
-
-lintQuantifiedWorkT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)
-                    => [Var] -> Transform c m Quantified String
-lintQuantifiedWorkT bs = readerT $ \ (Quantified bs' _) -> quantifiedT successT (lintClauseT (bs++bs')) (flip const)
-
-lintClauseT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)
-            => [Var] -> Transform c m Clause String
-lintClauseT bs = do
-    t <- readerT $ \case Equiv {} -> return $ promoteT ({- arr (mkCoreLams bs) >>> -} lintExprT) -- TODO: why does this break core lint?!
-                         _        -> return $ promoteT (lintQuantifiedWorkT bs)
-    (w1,w2) <- clauseT t t (const (,))
-    return $ unlines [w1,w2]
-
-------------------------------------------------------------------------------
-
 -- TODO: everything between here and instantiateDictsR needs to be rethought/removed
 
 -- TODO: this is used in century plugin, but otherwise should be removed
@@ -691,11 +647,9 @@
 markLemmaUsedT :: (HasLemmas m, Monad m) => LemmaName -> Used -> Transform c m a ()
 markLemmaUsedT nm u = modifyLemmaT nm id idR id (const u)
 
-markLemmaProvedT :: (HasLemmas m, Monad m) => LemmaName -> Transform c m a ()
-markLemmaProvedT nm = modifyLemmaT nm id idR (const Proven) id
+markLemmaProvenT :: (HasLemmas m, Monad m) => LemmaName -> Proven -> Transform c m a ()
+markLemmaProvenT nm p = modifyLemmaT nm id idR (const p) id
 
-markLemmaAssumedT :: (HasLemmas m, Monad m) => Bool -> LemmaName -> Transform c m a ()
-markLemmaAssumedT user nm = modifyLemmaT nm id idR (const (Assumed user)) id
 ------------------------------------------------------------------------------
 
 lemmaNameToQuantifiedT :: (HasLemmas m, Monad m) => LemmaName -> Transform c m x Quantified
diff --git a/src/HERMIT/Dictionary/WorkerWrapper/Common.hs b/src/HERMIT/Dictionary/WorkerWrapper/Common.hs
--- a/src/HERMIT/Dictionary/WorkerWrapper/Common.hs
+++ b/src/HERMIT/Dictionary/WorkerWrapper/Common.hs
@@ -157,7 +157,7 @@
     verifyOrCreateT u (fromString (show nm ++ "-assumption")) $ Lemma assumptionQ NotProven u False -- unproven, used, permanent
 
     wwFusionQ <- wwFusionQuantifiedT absE repE workRhs
-    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ (Assumed False) NotUsed False -- assumed, unused, permanent
+    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ BuiltIn NotUsed False -- assumed, unused, permanent
 
     return $ mkCoreLets [NonRec gId g, NonRec workId workRhs] newRhs
 
@@ -177,6 +177,6 @@
     verifyOrCreateT u (fromString (show nm ++ "-assumption")) $ Lemma assumptionQ NotProven u False -- unproven, used, permanent
 
     wwFusionQ <- wwFusionQuantifiedT absE repE (varToCoreExpr workId)
-    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ (Assumed False) NotUsed False -- assumed, unused, permanent
+    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ BuiltIn NotUsed False -- assumed, unused, permanent
 
     return $ mkCoreLets [NonRec workId repFixFE] newRhs
diff --git a/src/HERMIT/Kure.hs b/src/HERMIT/Kure.hs
--- a/src/HERMIT/Kure.hs
+++ b/src/HERMIT/Kure.hs
@@ -86,6 +86,7 @@
     , implT, implAllR
     , equivT, equivAllR
     , quantifiedT, quantifiedR
+    , clauseT, clauseR, forallVarsT
       -- * Applicative
       -- | Remove in 7.10
     , (<$>)
@@ -1359,3 +1360,23 @@
     getDynFlags = constT getDynFlags
 
 ---------------------------------------------------------------------
+
+-- | Original clause passed to function so it can decide how to handle connective.
+clauseT :: (Monad m, ExtendPath c Crumb) => Transform c m LCore a -> Transform c m LCore b -> (Clause -> a -> b -> d) -> Transform c m Clause d
+clauseT t1 t2 f = readerT $ \ cl -> case cl of
+                                      Conj{}  -> conjT  (extractT t1) (extractT t2) (f cl)
+                                      Disj{}  -> disjT  (extractT t1) (extractT t2) (f cl)
+                                      Impl{}  -> implT  (extractT t1) (extractT t2) (f cl)
+                                      Equiv{} -> equivT (extractT t1) (extractT t2) (f cl)
+
+clauseR :: (Monad m, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m LCore -> Rewrite c m Clause
+clauseR r1 r2 = readerT $ \case
+                             Conj{}  -> conjAllR (extractR r1) (extractR r2)
+                             Disj{}  -> disjAllR (extractR r1) (extractR r2)
+                             Impl{}  -> implAllR (extractR r1) (extractR r2)
+                             Equiv{} -> equivAllR (extractR r1) (extractR r2)
+
+-- | Lift a transformation over '[Var]' into a transformation over the universally quantified variables of a 'Quantified'.
+forallVarsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m [Var] b -> Transform c m Quantified b
+forallVarsT t = quantifiedT t successT const
+
diff --git a/src/HERMIT/Lemma.hs b/src/HERMIT/Lemma.hs
--- a/src/HERMIT/Lemma.hs
+++ b/src/HERMIT/Lemma.hs
@@ -102,28 +102,32 @@
                    }
 
 data Proven = Proven
-            | Assumed Bool -- ^ True = assumed by user, False = assumed by library/HERMIT for good reason
+            | Assumed -- ^ Assumed by user
+            | BuiltIn -- ^ Assumed by library/HERMIT
             | NotProven
     deriving (Eq, Typeable)
 
 instance Show Proven where
     show Proven = "Proven"
-    show (Assumed _) = "Assumed"
+    show Assumed = "Assumed"
+    show BuiltIn = "Built In"
     show NotProven = "Not Proven"
 
--- Ordering: NotProven < Assumed True < Assumed False < Proven
+instance Enum Proven where
+    toEnum 1 = Assumed
+    toEnum 2 = BuiltIn
+    toEnum 3 = Proven
+    toEnum _ = NotProven
+
+    fromEnum NotProven = 0
+    fromEnum Assumed = 1
+    fromEnum BuiltIn = 2
+    fromEnum Proven = 3
+
+-- Ordering: NotProven < Assumed < BuiltIn < Proven
 instance Ord Proven where
     compare :: Proven -> Proven -> Ordering
-    compare Proven    Proven    = EQ
-    compare (Assumed l) (Assumed r)
-        | l && (not r) = LT
-        | (not l) && r = GT
-        | otherwise = EQ
-    compare NotProven NotProven = EQ
-    compare Proven    _         = GT
-    compare _         Proven    = LT
-    compare NotProven _         = LT
-    compare _         NotProven = GT
+    compare p1 p2 = compare (fromEnum p1) (fromEnum p2)
 
 -- When conjuncting, result is as proven as the least of the two
 andP :: Proven -> Proven -> Proven
diff --git a/src/HERMIT/Libraries/Int.hs b/src/HERMIT/Libraries/Int.hs
--- a/src/HERMIT/Libraries/Int.hs
+++ b/src/HERMIT/Libraries/Int.hs
@@ -49,7 +49,7 @@
         appMN e = mkCoreApps e [m,n]
         appNM e = mkCoreApps e [n,m]
         mkEL l r = mkL (Equiv l r)
-        mkL cl = Lemma (Quantified [mId,nId] cl) (Assumed False) NotUsed False
+        mkL cl = Lemma (Quantified [mId,nId] cl) BuiltIn NotUsed False
         mkIL al ar cl cr = mkL (Impl (Quantified [] $ Equiv al ar) (Quantified [] $ Equiv cl cr))
 
     eqE <- findIdT "Data.Eq.==" >>= appToInt >>= appToDict
diff --git a/src/HERMIT/Shell/Command.hs b/src/HERMIT/Shell/Command.hs
--- a/src/HERMIT/Shell/Command.hs
+++ b/src/HERMIT/Shell/Command.hs
@@ -124,7 +124,7 @@
 #endif
 
     -- Load and run any scripts
-    setRunningScript $ Just []
+    setRunningScript $ Just [] -- suppress all output until after first scripts run
     sequence_ [ case fileName of
                  "abort"  -> parseScriptCLT "abort" >>= pushScript
                  "resume" -> parseScriptCLT "resume" >>= pushScript
@@ -134,8 +134,8 @@
               ] `catchFailHard` \ msg -> cl_putStrLn $ "Booting Failure: " ++ msg
 
     let -- Main proof input loop
-        loop :: InputT m ()
-        loop = do
+        loop :: Bool -> InputT m ()
+        loop firstInput = do
             el <- lift $ do tryM () announceProven
                             tryM () forceProofs
                             attemptM currentLemma
@@ -143,8 +143,7 @@
             mExpr <- lift popScriptLine
             case mExpr of
                 Nothing -> do -- no script running
-                    lift $ ifM isRunningScript (return ()) (showWindow Nothing)
-                            `catchFailHard` (cl_putStrLn . ("cannot showWindow: " ++))
+                    when firstInput $ lift $ showWindow Nothing
                     st <- lift get
                     mLine <- if cl_nav st
                              then liftIO getNavCmd
@@ -152,15 +151,17 @@
 
                     case mLine of
                         Nothing          -> lift $ performShellEffect Resume
-                        Just ('-':'-':_) -> loop
+                        Just ('-':'-':_) -> loop False
                         Just line        -> if all isSpace line
-                                            then loop
-                                            else lift (evalScript line `catchFailHard` cl_putStrLn) >> loop
-                Just e -> lift (runExprH e `catchFailHard` (\ msg -> setRunningScript Nothing >> cl_putStrLn msg)) >> loop
+                                            then loop False
+                                            else lift (evalScript line `catchFailHard` cl_putStrLn) >> loop False
+                Just e -> do
+                    lift (runExprH e `catchFailHard` (\ msg -> setRunningScript Nothing >> cl_putStrLn msg))
+                    loop True
 
     -- Start the CLI
     let settings = setComplete (completeWordWithPrev Nothing ws_complete completer) defaultSettings
-    runInputT settings loop
+    runInputT settings (loop True)
 
 -- | Like 'catchM', but checks the 'cl_failhard' setting and does so if needed.
 catchFailHard :: (MonadCatch m, CLMonad m) => m () -> (String -> m ()) -> m ()
@@ -190,7 +191,7 @@
   , interpM  $ \ (effect :: ShellEffect)        -> performShellEffect effect
   , interpM  $ \ (effect :: ScriptEffect)       -> performScriptEffect effect
   , interpEM $ \ (query :: QueryFun)            -> performQuery query
-  , interpEM $ \ (t :: UserProofTechnique)      -> performProofShellCommand $ PCUser t
+  , interpEM $ \ (t :: UserProofTechnique)      -> performProofShellCommand $ PCEnd $ UserProof t
   , interpEM $ \ (cmd :: ProofShellCommand)     -> performProofShellCommand cmd
   , interpEM $ \ (TransformLCoreStringBox tt)   -> performQuery (QueryString tt)
   , interpEM $ \ (TransformLCoreTCStringBox tt) -> performQuery (QueryString tt)
diff --git a/src/HERMIT/Shell/Externals.hs b/src/HERMIT/Shell/Externals.hs
--- a/src/HERMIT/Shell/Externals.hs
+++ b/src/HERMIT/Shell/Externals.hs
@@ -51,25 +51,25 @@
         [ "switch to navigate mode" ]
     , external "command-line"    (CLSModify $ \ st -> return $ Right $ st { cl_nav = False })
         [ "switch to command line mode" ]
-    , external "set-window"      (CLSModify setWindow)
+    , external "set-window"      (CLSModifyAndShow setWindow)
         [ "fix the window to the current focus" ]
     , external "top"             (Direction T)
         [ "move to root of current scope" ]
     , external "log"             (Inquiry showDerivationTree)
         [ "go back in the derivation" ]                                          .+ VersionControl
-    , external "back"            (CLSModify $ versionCmd Back)
+    , external "back"            (CLSModifyAndShow $ versionCmd Back)
         [ "go back in the derivation" ]                                          .+ VersionControl
-    , external "step"            (CLSModify $ versionCmd Step)
+    , external "step"            (CLSModifyAndShow $ versionCmd Step)
         [ "step forward in the derivation" ]                                     .+ VersionControl
-    , external "goto"            (CLSModify . versionCmd . Goto)
+    , external "goto"            (CLSModifyAndShow . versionCmd . Goto)
         [ "goto a specific step in the derivation" ]                             .+ VersionControl
-    , external "goto"            (CLSModify . versionCmd . GotoTag)
+    , external "goto"            (CLSModifyAndShow . versionCmd . GotoTag)
         [ "goto a specific step in the derivation by tag name" ]                 .+ VersionControl
     , external "tag"             (CLSModify . versionCmd . Tag)
         [ "name the current step in the derivation" ]                            .+ VersionControl
     , external "diff"            Diff
         [ "show diff of two ASTs" ]                                              .+ VersionControl
-    , external "set-pp-diffonly" (\ bStr -> CLSModify $ \ st ->
+    , external "set-pp-diffonly" (\ bStr -> CLSModifyAndShow $ \ st ->
         case reads bStr of
             [(b,"")] -> return $ Right $ setDiffOnly st b
             _        -> return $ Left $ CLError "valid arguments are True and False" )
@@ -87,7 +87,7 @@
             _        -> return $ Left $ CLError "valid arguments are True and False" )
         [ "set-auto-corelint <True|False>; False by default"
         , "run core lint type-checker after every rewrite, reverting on failure" ]
-    , external "set-pp"          (\ name -> CLSModify $ \ st ->
+    , external "set-pp"          (\ name -> CLSModifyAndShow $ \ st ->
         case M.lookup name pp_dictionary of
             Nothing -> return $ Left $ CLError $ "List of Pretty Printers: " ++ intercalate ", " (M.keys pp_dictionary)
             Just pp -> return $ Right $ flip setPrettyOpts (cl_pretty_opts st) $ setPretty st pp) -- careful to preserve the current options
@@ -108,20 +108,20 @@
     , external "dump-lemma" ((\pp nm fp r w -> getLemmaByNameT nm >>> liftPrettyH (pOptions pp) (ppLemmaT pp nm) >>> dumpT fp pp r w) :: PrettyPrinter -> LemmaName -> FilePath -> String -> Int -> TransformH LCoreTC ())
         [ "Dump named lemma to a file."
         , "dump-lemma <lemma-name> <filename> <pretty-printer> <renderer> <width>" ]
-    , external "set-pp-width" (\ w -> CLSModify $ \ st ->
+    , external "set-pp-width" (\ w -> CLSModifyAndShow $ \ st ->
             return $ Right $ setPrettyOpts st (updateWidthOption w (cl_pretty_opts st)))
         ["set the width of the screen"]
-    , external "set-pp-type" (\ str -> CLSModify $ \ st ->
+    , external "set-pp-type" (\ str -> CLSModifyAndShow $ \ st ->
         case reads str :: [(ShowOption,String)] of
             [(opt,"")] -> return $ Right $ setPrettyOpts st (updateTypeShowOption opt (cl_pretty_opts st))
             _          -> return $ Left $ CLError "valid arguments are Show, Abstract, and Omit")
         ["set how to show expression-level types (Show|Abstact|Omit)"]
-    , external "set-pp-coercion" (\ str -> CLSModify $ \ st ->
+    , external "set-pp-coercion" (\ str -> CLSModifyAndShow $ \ st ->
         case reads str :: [(ShowOption,String)] of
             [(opt,"")] -> return $ Right $ setPrettyOpts st (updateCoShowOption opt (cl_pretty_opts st))
             _          -> return $ Left $ CLError "valid arguments are Show, Abstract, and Omit")
         ["set how to show coercions (Show|Abstact|Omit)"]
-    , external "set-pp-uniques" (\ str -> CLSModify $ \ st ->
+    , external "set-pp-uniques" (\ str -> CLSModifyAndShow $ \ st ->
         case reads str of
             [(b,"")] -> return $ Right $ setPrettyOpts st ((cl_pretty_opts st) { po_showUniques = b } )
             _        -> return $ Left $ CLError "valid arguments are True and False")
diff --git a/src/HERMIT/Shell/KernelEffect.hs b/src/HERMIT/Shell/KernelEffect.hs
--- a/src/HERMIT/Shell/KernelEffect.hs
+++ b/src/HERMIT/Shell/KernelEffect.hs
@@ -69,11 +69,13 @@
                 putStrToConsole warns
 
             addAST ast'
+    ifM isRunningScript (return ()) (showWindow Nothing)
 
 setPath :: (Injection a LCoreTC, MonadCatch m, CLMonad m) => TransformH a LocalPathH -> ExprH -> m ()
 setPath t expr = do
     p <- prefixFailMsg "Cannot find path: " $ queryInContext (promoteT t) Never
     modifyLocalPath (<> p) expr
+    ifM isRunningScript (return ()) (showWindow Nothing)
 
 goUp :: (MonadCatch m, CLMonad m) => Direction -> ExprH -> m ()
 goUp T expr = modifyLocalPath (const mempty) expr
@@ -82,6 +84,7 @@
     case rel of
         SnocPath [] -> fail "cannot move up, at root of scope."
         SnocPath (_:cs) -> modifyLocalPath (const $ SnocPath cs) expr
+    ifM isRunningScript (return ()) (showWindow Nothing)
 
 beginScope :: (MonadCatch m, CLMonad m) => ExprH -> m ()
 beginScope expr = do
@@ -99,6 +102,7 @@
             let todos' = Unproven nm l c ls (p : base, mempty) : todos
             modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) todos' (cl_proofstack st) }
         _ -> fail "beginScope: impossible case!"
+    ifM isRunningScript (return ()) (showWindow Nothing)
 
 endScope :: (MonadCatch m, CLMonad m) => ExprH -> m ()
 endScope expr = do
@@ -122,6 +126,7 @@
                     let todos' = Unproven nm l c ls (base', p) : todos
                     modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) todos' (cl_proofstack st) }
         _ -> fail "endScope: impossible case!"
+    ifM isRunningScript (return ()) (showWindow Nothing)
 
 deleteAST :: (MonadCatch m, CLMonad m) => AST -> m ()
 deleteAST ast = gets cl_kernel >>= flip deleteK ast
diff --git a/src/HERMIT/Shell/Proof.hs b/src/HERMIT/Shell/Proof.hs
--- a/src/HERMIT/Shell/Proof.hs
+++ b/src/HERMIT/Shell/Proof.hs
@@ -17,11 +17,12 @@
     , withProofExternals
     , performProofShellCommand
     , forceProofs
-    , ProofShellCommand(PCUser)
+    , ProofShellCommand(PCEnd)
+    , ProofReason(UserProof)
     ) where
 
 import Control.Arrow hiding (loop, (<+>))
-import Control.Monad (forM, forM_, liftM, unless)
+import Control.Monad (forM, forM_, liftM)
 import Control.Monad.Error.Class (MonadError(..))
 import Control.Monad.State (MonadState, modify, gets)
 
@@ -57,16 +58,16 @@
 -- | Externals that get us into the prover shell.
 externals :: [External]
 externals = map (.+ Proof)
-    [ external "prove-lemma" (CLSModify . interactiveProofIO)
+    [ external "prove-lemma" (CLSModifyAndShow . interactiveProofIO)
         [ "Proof a lemma interactively." ]
     ]
 
 -- | Externals that are added to the dictionary only when in interactive proof mode.
 proof_externals :: [External]
 proof_externals = map (.+ Proof)
-    [ external "lemma" (PCEnd . Right . (Obligation,))
+    [ external "lemma" (PCEnd . LemmaProof Obligation)
         [ "Prove lemma by asserting it is alpha-equivalent to an already proven lemma." ]
-    , external "lemma-unsafe" (PCEnd . Right . (UnsafeUsed,))
+    , external "lemma-unsafe" (PCEnd . LemmaProof UnsafeUsed)
         [ "Prove lemma by asserting it is alpha-equivalent to an already proven lemma." ] .+ Unsafe
     , external "induction" (PCInduction . cmpString2Var :: String -> ProofShellCommand)
         [ "Perform induction on given universally quantified variable."
@@ -84,11 +85,11 @@
         [ "Split an assumed lemma which is a conjunction/disjunction." ]
     , external "split-assumed" PCSplitAssumed
         [ "Split an assumed lemma which is a conjunction/disjunction." ]
-    , external "end-proof" (PCEnd (Left False))
+    , external "end-proof" (PCEnd Reflexivity)
         [ "check for alpha-equality, marking the lemma as proven" ]
-    , external "end-case" (PCEnd (Left False))
+    , external "end-case" (PCEnd Reflexivity)
         [ "check for alpha-equality, marking the proof case as proven" ]
-    , external "assume" (PCEnd (Left True))
+    , external "assume" (PCEnd UserAssume)
         [ "mark lemma as assumed" ]
     ]
 
@@ -136,16 +137,17 @@
         forM_ nls' $ \ (nm,l) -> pushProofStack (Unproven nm l c' [] mempty)
 
 -- | Verify that the lemma has been proven. Throws an exception if it has not.
-endProof :: (MonadCatch m, CLMonad m) => Either Bool (Used,LemmaName) -> ExprH -> m ()
+endProof :: (MonadCatch m, CLMonad m) => ProofReason -> ExprH -> m ()
 endProof reason expr = do
     Unproven nm (Lemma q _ _ temp) c ls _ : _ <- getProofStack
     let msg = "The two sides of " ++ quoteShow nm ++ " are not alpha-equivalent."
         deleteOr tr = if temp then constT (deleteLemma nm) else tr
         t = case reason of
-                Left assumed
-                    | assumed   -> deleteOr (markLemmaAssumedT True nm)
-                    | otherwise -> setFailMsg msg verifyQuantifiedT >> deleteOr (markLemmaProvedT nm)
-                Right (u,nm') -> verifyEquivalentT u nm' >> deleteOr (markLemmaProvedT nm)
+                UserAssume -> deleteOr (markLemmaProvenT nm Assumed)
+                Reflexivity -> setFailMsg msg verifyQuantifiedT >> deleteOr (markLemmaProvenT nm Proven)
+                LemmaProof u nm' -> verifyEquivalentT u nm' >> deleteOr (markLemmaProvenT nm Proven)
+                UserProof up -> let UserProofTechnique tr = up
+                                in extractT tr >> deleteOr (markLemmaProvenT nm Proven)
     queryInFocus (constT (withLemmas (M.fromList ls) $ applyT t c q) :: TransformH Core ())
                  (Always $ unparseExprH expr ++ " -- proven " ++ quoteShow nm)
     _ <- popProofStack
@@ -165,15 +167,6 @@
           go PCConjunction        = proveConjunction str
           go (PCInstAssumed i v cs) = instAssumed i v cs str
           go (PCSplitAssumed i)   = splitAssumed i str
-          go (PCUser prf)         = do
-                let UserProofTechnique t = prf -- may add more constructors later
-                -- note: we assume that if 't' completes without failing,
-                -- the lemma is proved, we don't actually check
-                todo : _ <- getProofStack
-                queryInFocus (inProofFocusT todo t >> unless (lemmaT $ ptLemma todo) (markLemmaProvedT (ptName todo)))
-                             (Changed str)
-                _ <- popProofStack
-                cl_putStrLn $ "Successfully proven: " ++ show (ptName todo)
           go (PCEnd why)          = endProof why expr
 
 proveConsequent :: (MonadCatch m, CLMonad m) => String -> m ()
@@ -182,7 +175,7 @@
     (c, Impl ante con) <- setFailMsg "not an implication" $
                           queryInFocus (inProofFocusT todo (contextT &&& projectT)) Never
     let nm = ptName todo
-        ls = (nm <> "-antecedent", Lemma ante (Assumed False) NotUsed True) : ptAssumed todo
+        ls = (nm <> "-antecedent", Lemma ante BuiltIn NotUsed True) : ptAssumed todo
     (k,ast) <- gets (cl_kernel &&& cl_cursor)
     addAST =<< tellK k expr ast
     _ <- popProofStack
@@ -269,7 +262,7 @@
                 -- TODO rethink the discardUniVars
 
         let nms = [ fromString ("ind-hyp-" ++ show n) | n :: Int <- [0..] ]
-            hypLemmas = zip nms $ zipWith4 Lemma qs (repeat (Assumed False)) (repeat NotUsed) (repeat True)
+            hypLemmas = zip nms $ zipWith4 Lemma qs (repeat BuiltIn) (repeat NotUsed) (repeat True)
             lemmaName = fromString $ show nm ++ "-induction-case-" ++ caseName
             caseLemma = Lemma (mkQuantified (delete i bs ++ vs) lhsE rhsE) NotProven Obligation True
 
@@ -306,11 +299,13 @@
     | PCConjunction
     | PCSplitAssumed Int
     | PCInstAssumed Int (Var -> Bool) CoreString
-    | PCUser UserProofTechnique
-    | PCEnd (Either Bool (Used,LemmaName)) -- ^ Left True = assume this lemma
-                                           --   Left False = check for alpha-equivalence
-                                           --   Right (u,nm) = try to prove with given lemma, marking it u
+    | PCEnd ProofReason
     deriving Typeable
+
+data ProofReason = UserProof UserProofTechnique -- ^ Run the technique, mark Proven if succeeds
+                 | UserAssume                   -- ^ Assume
+                 | Reflexivity                  -- ^ Check for alpha-equivalence first
+                 | LemmaProof Used LemmaName    -- ^ Used should be 'UnsafeUsed' or 'Obligation'
 
 -- keep abstract to avoid breaking things if we modify this later
 newtype UserProofTechnique = UserProofTechnique (TransformH LCoreTC ())
diff --git a/src/HERMIT/Shell/ScriptToRewrite.hs b/src/HERMIT/Shell/ScriptToRewrite.hs
--- a/src/HERMIT/Shell/ScriptToRewrite.hs
+++ b/src/HERMIT/Shell/ScriptToRewrite.hs
@@ -11,7 +11,6 @@
     , popScriptLine
     , pushScriptLine
     , pushScript
-    , runScript
     , fileToScript
     , scriptToRewrite
     , ScriptEffect(..)
@@ -65,10 +64,6 @@
 --   The script is given the same name as the filepath.
 loadAndRun :: FilePath -> ScriptEffect
 loadAndRun fp = SeqMeta [LoadFile fp fp, RunScript fp]
-
-runScript :: MonadState CommandLineState m => (ExprH -> m ()) -> m ()
-runScript run = go
-    where go = popScriptLine >>= maybe (return ()) (\e -> run e >> go)
 
 popScriptLine :: MonadState CommandLineState m => m (Maybe ExprH)
 popScriptLine = gets cl_running_script >>= maybe (return Nothing)
diff --git a/src/HERMIT/Shell/ShellEffect.hs b/src/HERMIT/Shell/ShellEffect.hs
--- a/src/HERMIT/Shell/ShellEffect.hs
+++ b/src/HERMIT/Shell/ShellEffect.hs
@@ -36,11 +36,12 @@
 ----------------------------------------------------------------------------------
 
 data ShellEffect :: * where
-    Abort      :: ShellEffect
-    CLSModify  :: (CommandLineState -> IO (Either CLException CommandLineState)) -> ShellEffect
-    PluginComp :: PluginM () -> ShellEffect
-    Continue   :: ShellEffect
-    Resume     :: ShellEffect
+    Abort             :: ShellEffect
+    CLSModify         :: (CommandLineState -> IO (Either CLException CommandLineState)) -> ShellEffect
+    CLSModifyAndShow  :: (CommandLineState -> IO (Either CLException CommandLineState)) -> ShellEffect
+    PluginComp        :: PluginM () -> ShellEffect
+    Continue          :: ShellEffect
+    Resume            :: ShellEffect
     deriving Typeable
 
 instance Extern ShellEffect where
@@ -55,7 +56,11 @@
 performShellEffect Resume = announceUnprovens >> gets cl_cursor >>= resume
 performShellEffect Continue = announceUnprovens >> get >>= continue
 
-performShellEffect (CLSModify f)  = get >>= liftAndCatchIO . f >>= either throwError put
+performShellEffect (CLSModify f) = get >>= liftAndCatchIO . f >>= either throwError put
+
+performShellEffect (CLSModifyAndShow f) = do
+    get >>= liftAndCatchIO . f >>= either throwError put
+    ifM isRunningScript (return ()) (showWindow Nothing)
 
 performShellEffect (PluginComp m) = pluginM m
 
diff --git a/src/HERMIT/Shell/Types.hs b/src/HERMIT/Shell/Types.hs
--- a/src/HERMIT/Shell/Types.hs
+++ b/src/HERMIT/Shell/Types.hs
@@ -25,6 +25,7 @@
 import Control.Monad.Trans.Except (ExceptT(..), runExceptT)
 
 import Data.Dynamic
+import Data.List (intercalate)
 import qualified Data.Map as M
 import Data.Maybe (fromMaybe, isJust)
 import Data.Monoid (mempty, (<>))
@@ -507,14 +508,20 @@
         _ -> fail "currentLemma: unproven lemma not on top of stack!"
 
 announceProven :: (MonadCatch m, CLMonad m) => m ()
-announceProven = getProofStack >>= go
-    where go (MarkProven nm temp : r) = do
-            queryInFocus (if temp then constT (deleteLemma nm) else modifyLemmaT nm id idR (const Proven) id :: TransformH Core ())
-                         (Always $ "-- proven " ++ quoteShow nm) -- comment in script
-            -- take it off the stack for the new AST
-            modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) r (cl_proofstack st) }
-            cl_putStrLn ("Successfully proven: " ++ show nm) >> go r
-          go _ = return ()
+announceProven = getProofStackEmpty >>= go []
+    where go ps (MarkProven nm temp : r) = do
+            let t = if temp then constT (deleteLemma nm) else modifyLemmaT nm id idR (const Proven) id
+            go ((nm,t):ps) r
+          go ps r = case ps of
+                        [] -> return ()
+                        _  -> do -- adjust the stack for the existing AST, because we don't want
+                                 -- to replay these after a 'goto'!
+                                 let (nms, ts) = unzip $ reverse ps
+                                     commaNames f = intercalate ", " (map f nms)
+                                 modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) r (cl_proofstack st) }
+                                 queryInFocus (sequence_ ts :: TransformH Core ())
+                                              (Always $ "-- proven " ++ commaNames quoteShow)
+                                 cl_putStrLn ("Successfully proven: " ++ commaNames show)
 
 announceUnprovens :: (MonadCatch m, CLMonad m) => m ()
 announceUnprovens = do
@@ -522,7 +529,7 @@
     sf <- gets cl_safety
     case sf of
         StrictSafety -> do
-            let ls = [ nl | nl@(_,Lemma _ p u _) <- M.toList m, p `elem` [NotProven, Assumed True], u /= NotUsed ]
+            let ls = [ nl | nl@(_,Lemma _ p u _) <- M.toList m, p `elem` [NotProven, Assumed], u /= NotUsed ]
             forM_ ls $ \ nl@(nm,_) -> do
                 cl_putStrLn $ "Fatal: Lemma " ++ show nm ++ " has not been proven, but was used."
                 printLemma stdout c mempty nl
@@ -533,7 +540,7 @@
                 cl_putStrLn $ "Fatal: Lemma " ++ show nm ++ " has not been proven, but was used."
                 printLemma stdout c mempty nl
             unless (null np) abort -- don't finish if this happens
-            let as = [ nl | nl@(_,Lemma _ (Assumed True) u _) <- M.toList m, u /= NotUsed ]
+            let as = [ nl | nl@(_,Lemma _ Assumed u _) <- M.toList m, u /= NotUsed ]
             forM_ as $ \ nl@(nm,_) -> do
                 cl_putStrLn $ "Warning: Lemma " ++ show nm ++ " was assumed but not proven."
                 printLemma stdout c mempty nl