         (if value (whatif--simplify then bindings)
           (whatif--simplify else bindings)))
        (`(unknown ,_) (list 'unknown form))))
+    ;; Remove pointless values in progn, e.g.
+    ;; (progn nil (foo) (bar)) -> (progn (foo) (bar))
+    (`(progn . ,exprs)
+     (let (simplified-exprs current)
+       ;; Evaluate every expression in the progn body.
+       (dolist (expr exprs)
+         (setq current (whatif--simplify expr bindings))
+         ;; If we evaluated the expression to a value, just throw it
+         ;; away.
+         (pcase current
+           (`(unknown ,subform)
+            (push (list 'unknown subform) simplified-exprs))))
+       ;; If the last expression was a value, we still need to return
+       ;; it.
+       (pcase current
+         (`(value ,value)
+          (push (list 'value value) simplified-exprs)))
+       (setq simplified-exprs (nreverse simplified-exprs))
+
+       (if (eq 1 (length simplified-exprs))
+           (car simplified-exprs)
+         (list 'unknown `(progn ,@(--map (nth 1 it) simplified-exprs))))))
+    
+    ;; Eliminate or simplify a when statement if we can evaluate the
+    ;; condition.
+    (`(when ,cond . ,body)
+     (pcase (whatif--simplify cond bindings)
+       (`(value ,value)
+        (if value (whatif--simplify (cons 'progn body) bindings)
+          (list 'value nil)))
+       (`(unknown ,_) (list 'unknown form))))
+    
     (_ (list 'unknown form))))
 
 (whatif--simplify '(if 1 2 3) nil)

   (equal
    (whatif--simplify '(if x y z) '((x . 42)))
    (list 'unknown 'y))))

  "Simplify FORM in the context of BINDINGS using partial application.
Loops are not executed and side-effecting functions are not run."
  (pcase form
    ;; nil and t evaluate to themselves.
    (`nil (list 'value nil))
    (`t (list 'value t))
    ;; Literal keywords, strings and numbers evaluate to themselves.
    ((pred keywordp)
     (list 'value form))
    ((pred stringp)
     (list 'value form))
    ((pred numberp)
     (list 'value form))
    ;; We can evaluate a symbol if it is present in BINDINGS.
    ((pred symbolp)
     (if (assoc form bindings)
         (list 'value (alist-get form bindings))
