diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Revision history for bisect-binary
 
+## 0.1.0.1
+
+* Fix bugs in `Intervals.hs` found by formal verification with Coq.
+
 ## 0.1
 
 * First version.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -10,7 +10,7 @@
 should be doing. If it does, then you know that the interesting parts are in
 another part of the file.
 
-`binary-binary` assists in this process by doing the book-keeping and zeroing
+`bisect-binary` assists in this process by doing the book-keeping and zeroing
 out parts of the file.
 
 
diff --git a/bisect-binary.cabal b/bisect-binary.cabal
--- a/bisect-binary.cabal
+++ b/bisect-binary.cabal
@@ -1,5 +1,5 @@
 name:                bisect-binary
-version:             0.1
+version:             0.1.0.1
 synopsis:            Determine relevant parts of binary data
 description:
      This little program helps with the following task:
diff --git a/src/Intervals.hs b/src/Intervals.hs
--- a/src/Intervals.hs
+++ b/src/Intervals.hs
@@ -1,5 +1,16 @@
 {-# LANGUAGE LambdaCase, DeriveGeneric #-}
 
+-- |
+-- This module provides an (efficient?) (compact?) representation of sets of
+-- file offsets, together with a few basic operations.
+--
+-- The representation is a sorted list of disjoint, non-adjacent intervals.
+--
+-- The operations 'isEmpty', 'fullIntervals', 'nullInterval', 'subSetOf',
+-- 'union', 'intersection' and 'subtract' were formally proven correct using
+-- @hs-to-coq@:
+-- <https://github.com/antalsz/hs-to-coq/tree/20f8eced04e51289d81ce117861c82c2ea24c4df/examples/intervals>
+-- (Three bugs were found in the process.)
 module Intervals where
 
 import qualified Data.ByteString.Lazy as BS
@@ -52,9 +63,11 @@
         | to i1 < to i2 = go (i2:is2) (i1:is1)
         -- disjoint
         | from i1 >= to i2 = go (i1:is1) is2
+        -- subset
+        | to i1 == to i2 = I f' (to i2) : go is1 is2
         -- overlapping
         | otherwise = I f' (to i2) : go (i1 { from = to i2} : is1) is2
-            where f' = max (from i1) (from i2)
+      where f' = max (from i1) (from i2)
 
 
 union :: Intervals -> Intervals -> Intervals
@@ -69,7 +82,7 @@
         | from i1 > to i2 = i2 : go (i1:is1) is2
         -- overlapping
         | otherwise  = go (i1 { from = f'} : is1) is2
-            where f' = min (from i1) (from i2)
+      where f' = min (from i1) (from i2)
 
 subtract :: Intervals -> Intervals -> Intervals
 subtract (Intervals is1) (Intervals is2) = Intervals $ go is1 is2
@@ -84,12 +97,12 @@
         -- i1 contained in i2
         | from i2 <= from i1 , to i1 <= to i2 = go is1 (i2:is2)
         -- i2 covers beginning of i1
-        | from i1 >= from i2 = i1 { from = to i2} : go is1 is2
+        | from i1 >= from i2 = go (i1 { from = to i2} : is1) is2
         -- i2 covers end of i1
         | to i1 <= to i2     = i1 { to = from i2} : go is1 (i2:is2)
         -- i2 in the middle of i1
         | otherwise = I (from i1) (from i2) :
-                      I (to i2)   (to i1) : go is1 is2
+                      go (I (to i2) (to i1) : is1) is2
 
 
 setZeros :: BS.ByteString -> Intervals -> BS.ByteString
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -163,8 +163,13 @@
                     steps log'
                     -- code smell
                     liftIO $ exitSuccess
+                Just 'F' -> do
+                    let log' = log { lgLogs = filter leOk (lgLogs log) }
+                    steps log'
+                    -- code smell
+                    liftIO $ exitSuccess
                 Just '?' -> do
-                    outputStrLn "Keys: Y: good. N: bad. R: rerun command. U: Undo. Q: Quit"
+                    outputStrLn "Keys: Y: good. N: bad. R: rerun command. U: Undo. F: Forget negatives Q: Quit"
                     loop
                 _ -> loop
 
@@ -179,7 +184,7 @@
                 (if done then "" else printf "%7dB new" (size toTry))
                 nonZeroBytes
                 (if barw > 5 then braille barw len conservative toTry else "")
-                (if done then "" else " [YNRUQ?] ")
+                (if done then "" else " [YNRUFQ?] ")
 
 
         -- Single step of the main loop
@@ -197,10 +202,31 @@
           where
             digest = digestLog log
 
+        lastStep :: Log -> InputT IO ()
+        lastStep log = fix $ \loop -> do
+            getInputChar "Done! [UFQ?]" >>= pure . fmap toUpper >>= \case
+                Just 'Q' -> do
+                    revert (digestLog log)
+                    liftIO $ exitSuccess
+                Just 'U' -> do
+                    let log' = log { lgLogs = init (lgLogs log) }
+                    steps log'
+                    -- code smell
+                    liftIO $ exitSuccess
+                Just 'F' -> do
+                    let log' = log { lgLogs = filter leOk (lgLogs log) }
+                    steps log'
+                    -- code smell
+                    liftIO $ exitSuccess
+                Just '?' -> do
+                    outputStrLn "Keys: U: Undo. F: Forget negatives Q: Quit"
+                    loop
+                _ -> loop
+
         -- Main loop
         steps log = do
-            foldM_ step log (intervalsToTry len)
-            outputStrLn $ printf "Done!"
+            log' <- foldM step log (intervalsToTry len)
+            lastStep log'
             -- TODO: What now?