 
 (defun fstar-subp-advance-until (pos)
   "Submit or retract blocks to/from prover until POS."
+  (fstar-subp-start)
   (save-excursion
     (goto-char (fstar-subp-unprocessed-beginning))
     (let ((found (cl-loop do (fstar-subp-skip-comments-and-whitespace)

(defun fstar-subp-advance-or-retract-to-point ()
  "Advance or retract proof state to reach point."
  (interactive)
  (let ((limit (fstar-subp-unprocessed-beginning)))
    (cond
     ((<= (point) limit) (fstar-subp-retract-until (point)))

(defun fstar-subp-advance-next ()
  "Process buffer until `fstar-subp-block-sep'."
  (interactive)
  (fstar-subp-start)
  (goto-char (fstar-subp-unprocessed-beginning))
  (fstar-subp-skip-comments-and-whitespace)
  (-if-let* ((next-start (re-search-forward fstar-subp-block-sep nil t)))
