diff --git a/.ocamlformat b/.ocamlformat
index f2116634..3d6101e9 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,2 +1,2 @@
-version=0.27.0
+version=0.28.1
 profile=default
diff --git a/.vscode/cspell.json b/.vscode/cspell.json
index 4bf3f7c3..a4ba0950 100644
--- a/.vscode/cspell.json
+++ b/.vscode/cspell.json
@@ -1,14 +1,51 @@
 {
-    "words": [
-        "tlaplus",
-        "tlaps",
-        "tlapm",
-        "zenon",
-        "opam",
-        "ocaml",
-        "caml",
-        "sandboxing",
-        "sprintf",
-        "printexc"
-    ]
+  "words": [
+    "tlaplus",
+    "tlaps",
+    "tlapm",
+    "zenon",
+    "opam",
+    "ocaml",
+    "caml",
+    "sandboxing",
+    "sprintf",
+    "printexc",
+    "Anoninst",
+    "Hashtbl",
+    "Pcase",
+    "Recursives",
+    "Submod",
+    "Tuply",
+    "failwith",
+    "iteri",
+    "mapi",
+    "modunit",
+    "naxs",
+    "assm",
+    "disj",
+    "Actplus",
+    "Cdot",
+    "Defn",
+    "Deque",
+    "Gteq",
+    "Leadsto",
+    "Lteq",
+    "Notmem",
+    "Setminus",
+    "Tquant",
+    "Tsub",
+    "Uminus",
+    "Unprimable",
+    "noprops",
+    "stepno",
+    "wheredef",
+    "forall",
+    "unditto",
+    "dvar",
+    "filteri",
+    "bpragma",
+    "alcotest",
+    "yojson",
+    "patdiff"
+  ]
 }
diff --git a/Makefile b/Makefile
index ca333260..f45e9f99 100644
--- a/Makefile
+++ b/Makefile
@@ -22,7 +22,7 @@ opam-update: # Update the package lists and install updates.
 	opam upgrade
 
 opam-deps:
-	opam install ./ --deps-only --yes --working-dir
+	opam install ./ --deps-only --with-test --yes --working-dir
 
 opam-deps-opt:
 	opam install --yes eio_main lsp
diff --git a/dune-project b/dune-project
index 63304037..061e413a 100644
--- a/dune-project
+++ b/dune-project
@@ -51,7 +51,10 @@
   ppx_inline_test
   ppx_assert
   ppx_deriving
-  ounit2)
+  (ounit2 :with-test)
+  (alcotest :with-test)
+  (ocolor :with-test)
+  (patdiff :with-test))
  (depopts
   lsp         ; https://github.com/ocaml/ocaml-lsp
   eio_main))  ; https://github.com/ocaml-multicore/eio, only available on OCaml version >= 5.
diff --git a/lsp/doc/README.md b/lsp/doc/README.md
new file mode 100644
index 00000000..95b9b230
--- /dev/null
+++ b/lsp/doc/README.md
@@ -0,0 +1,82 @@
+# Proof Decomposition
+
+The general idea is to keep the decision on making new proof levels for the user.
+Thus, if possible, the decomposition commands will try to refine the goal at the current level.
+
+Commands for introducing/reducing levels:
+
+- Convert the leaf proof to steps.
+  This introduces a new level into the proof.
+- Convert QED-only steps to a leaf proof.
+  This simplifies proof. If only a single step (QED) is left,
+  then there is no point in keeping the proof with the additional level introduced.
+
+# Decomposition by the goal
+
+Decomposition by the goal works by invoking code actions at the QED step of the current level.
+This is because during the steps at that level, the goal is refined, thus the ultimate goal
+is known at the QED step, and not at the upped-level step which is decomposed.
+Decompose goal is a single command for the user, but it works dependent on the structure of the goal:
+
+## Goal is implication
+
+The step with a goal `G == P => Q` and proof
+
+```tla
+<l>q. QED Proof
+```
+
+is transformed to
+
+```tla
+<l>x. SUFFICES ASSUME P PROVE Q BY DEF G
+<l>q. QED Proof
+```
+
+or if no operator expansion is needed:
+
+```tla
+<l>x. HAVE P
+<l>q. QED Proof
+```
+
+## Goal is conjunction
+
+If the goal is `P == P1 /\ P2 /\ ... Pn` with the proof
+
+```tla
+<l>q. QED ProofP
+```
+
+then it is transformed to steps (inserted before the QED):
+
+```tla
+<l>1. P1 ProofP
+<l>2. P2 ProofP
+...
+<l>n. Pn ProofP
+<l>q. QED BY <l>1, <l>2, ... <l>n DEF P
+```
+
+Here `DEF P` is only added, of the goal was an operator, which should be expanded.
+All the proof labels are introduced to be unused at that level.
+
+## Goal is disjunction
+
+Assume negations, prove the last disjunct.
+
+## Goal is equivalence
+
+Prove as conjunction of two implications.
+
+## Goal is forall
+
+TAKE or SUFFICE, depending of a need to expand something.
+
+## Goal is exists
+
+TODO: ...
+
+# Decomposition by the assumptions
+
+Only unused assumptions are proposed for the decomposition?
diff --git a/lsp/lib/analysis/step_decompose/of_assm.ml b/lsp/lib/analysis/step_decompose/of_assm.ml
new file mode 100644
index 00000000..911d1af1
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/of_assm.ml
@@ -0,0 +1,397 @@
+open Util
+
+(** Transform context so that all the hypotheses become hidden. That's to make
+    printed expression as small/compact as possible. *)
+let make_cx_hidden (cx : TL.Expr.T.ctx) : TL.Expr.T.ctx =
+  let open TL.Expr.T in
+  cx
+  |> TL.Util.Deque.map @@ fun _ hyp ->
+     match unwrap hyp with
+     | Fresh (_, _, _, _) | FreshTuply (_, _) | Flex _ -> hyp
+     | Defn (defn, wheredef, _, export) ->
+         TL.Property.( @@ ) (Defn (defn, wheredef, Hidden, export)) hyp
+     | Fact (expr, _, time) ->
+         TL.Property.( @@ ) (Fact (expr, Hidden, time)) hyp
+
+(** Limit length of a title, when referring to expressions. *)
+let limit_title title =
+  let max_len = 50 in
+  if String.length title > max_len then String.sub title 0 (max_len - 1) ^ "…"
+  else title
+
+(** Propose the decomposition Code Action for an assumption which is in the form
+    of conjunction. If we have an assumption
+    {v
+      A /\ B /\ ...
+    v}
+    with the current proof [pf], we will add steps before the QED step:
+    {v
+      <1>a. A [pf]
+      <1>b. B [pf]
+      ...
+    v} *)
+let cas_of_assm_conj (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    cx conjuncts =
+  (* TODO: Stop proposing the conjunction... *)
+  (* TODO: Name code actions by the nearest definition? *)
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let ps_proof = PS.proof ps |> Option.get in
+  let conjuncts = flatten_op_list Conj conjuncts in
+  let add_steps_rewrite =
+    conjuncts
+    |> List.map (fun conj ->
+        let step_no = Seq_acc.take step_names in
+        let step =
+          TL.Proof.T.Assert (Sequent.of_goal conj, ps_proof) |> noprops
+        in
+        (step_no, step))
+    |> pp_proof_steps_before ps cx
+  in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx
+      (`Usable
+         Usable.(
+           empty
+           |> add_steps (Seq_acc.acc step_names)
+           |> add_defs_from_pf ps_proof))
+  in
+  let title_ex = make_conjunction conjuncts in
+  let title =
+    Fmt.str "⤮ Split (∧): %a" (Debug.pp_expr_text (make_cx_hidden cx)) title_ex
+    |> limit_title
+  in
+  let ca =
+    ca_edits ~uri ~title ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+(** Propose proof decomposition Code Action for an assumption in the form of
+    disjunction.
+    - The proof is split to multiple steps "by cases", in the same level as the
+      QED step for which the action is proposed.
+    - The decomposition is only proposed if the current context don't have one
+      of the disjuncts among the assumptions. This way we don't repeat proposing
+      the same.
+
+    Thus, if we have an assumption
+    {v
+      A \/ B \/ ...
+    v}
+    with the current proof [pf], we will add steps before the QED step:
+    {v
+      <1>a. CASE A [pf + <1>a]
+      <1>b. CASE B [pf + <1>b]
+      ...
+      <1> QED [<1>a, <1>b, ... + defs from pf]
+    v} *)
+let cas_of_assm_disj (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    cx disjuncts =
+  (* TODO: Stop proposing the disjunction... *)
+  (* TODO: Name code actions by the nearest definition? *)
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let ps_proof = PS.proof ps |> Option.get in
+  let disjuncts = flatten_op_list Disj disjuncts in
+  let add_steps_rewrite =
+    disjuncts
+    |> List.map (fun disj ->
+        let step_no = Seq_acc.take step_names in
+        let step_pf =
+          Usable.(empty |> add_steps [ step_no ] |> add_to_pf ps_proof)
+        in
+        let step = TL.Proof.T.Pcase (disj, step_pf) |> noprops in
+        (step_no, step))
+    |> pp_proof_steps_before ps cx
+  in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx
+      (`Proof
+         Usable.(
+           empty |> add_steps (Seq_acc.acc step_names) |> add_to_pf ps_proof))
+  in
+  let title_ex = make_disjunction disjuncts in
+  let title =
+    Fmt.str "⤮ Case split (∨): %a"
+      (Debug.pp_expr_text (make_cx_hidden cx))
+      title_ex
+    |> limit_title
+  in
+  let ca =
+    ca_edits ~uri ~title ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+(** Propose use of an assumption in the form of an implication. Thus, if we have
+    assumption
+    {v
+      A => B => ... => C
+    v}
+    with the current proof [pf] we will produce
+    {v
+      <1>a. C
+        <2>a. A [pf]
+        <2>b. B [pf]
+        ...
+        <2> QED [<2>a, <2>b, ... + pf]
+      <1> QED [<1>a + pf]
+    v} *)
+let cas_of_assm_implies (uri : LspT.DocumentUri.t) (ps : PS.t)
+    (ps_parent : PS.t) cx args =
+  let open TL in
+  let antecedents, consequent =
+    match args |> flatten_op_list Implies |> List.rev with
+    | c :: a -> (List.rev a, c)
+    | [] -> assert false
+  in
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let ps_proof = PS.proof ps |> Option.get in
+  let add_steps_rewrite =
+    let step_no = Seq_acc.take step_names in
+    let step_pf =
+      let sub_stepno_seq =
+        PS.stepno_seq_under_stepno (Some step_no) |> Seq_acc.make
+      in
+      let sub_steps =
+        antecedents
+        |> List.mapi @@ fun i antecedent ->
+           let antecedent =
+             (* On the shift and cx. My [KP] guess follows:
+               - Each assert takes 1 bump (1 for main step, and 1 for each sub-step)
+               - Each named step does a bump for a name (of a step).
+               - The current step has the name, but not the assert yet, thus +1.
+             *)
+             antecedent |> Expr.Subst.(app_expr (shift (2 + (i * 2) + 1)))
+           in
+           let sn = Seq_acc.take sub_stepno_seq in
+           Proof.T.(Assert (Sequent.of_goal antecedent, ps_proof))
+           |> noprops |> with_stepno sn
+      in
+      let step_qed =
+        let pf =
+          Usable.(
+            empty
+            |> add_steps (Seq_acc.acc sub_stepno_seq)
+            |> add_to_pf ps_proof)
+        in
+        let sn = Seq_acc.take sub_stepno_seq in
+        Proof.T.Qed pf |> noprops |> with_stepno sn
+      in
+      Proof.T.Steps (sub_steps, step_qed) |> noprops
+    in
+    let step =
+      Proof.T.(Assert (Sequent.of_goal consequent, step_pf)) |> noprops
+    in
+    [ (step_no, step) ] |> pp_proof_steps_before ps cx
+  in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx
+      (`Proof
+         Usable.(
+           empty |> add_steps (Seq_acc.acc step_names) |> add_to_pf ps_proof))
+  in
+  let title_ex =
+    Expr.T.(Apply (Internal Builtin.Implies |> noprops, args)) |> noprops
+  in
+  let title =
+    Fmt.str "⤮ Use (⇒): %a" (Debug.pp_expr_text (make_cx_hidden cx)) title_ex
+    |> limit_title
+  in
+  let ca =
+    ca_edits ~uri ~title ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+(** For each assumption in the form of existential quantifier,
+    {v
+      \A x \in X : P(x)
+    v}
+    and [pf] as the current proof, we introduce
+    {v
+      <1>a. PICK x \in X : P(x)
+        <2>1. X # {}
+        <2>2. QED [pf + <2>1]
+    v} *)
+let cas_of_assm_forall (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    cx bs ex =
+  let open TL in
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let ps_proof = PS.proof ps |> Option.get in
+  let add_steps_rewrite =
+    let step_no = Seq_acc.take step_names in
+    let step_pf =
+      let sub_stepno_seq =
+        PS.stepno_seq_under_stepno (Some step_no) |> Seq_acc.make
+      in
+      let step_exists =
+        let _, bs =
+          (* See note in [cas_of_assm_implies]. *)
+          bs |> Expr.Subst.(app_bounds (shift (2 + (0 * 2) + 1)))
+        in
+        let goal =
+          Expr.T.(Quant (Exists, bs, Internal Builtin.TRUE |> noprops))
+          |> noprops
+        in
+        let sn = Seq_acc.take sub_stepno_seq in
+        Proof.T.Assert (Sequent.of_goal goal, ps_proof)
+        |> noprops |> with_stepno sn
+      in
+      let step_qed =
+        let pf =
+          Usable.(
+            empty
+            |> add_steps (Seq_acc.acc sub_stepno_seq)
+            |> add_to_pf ps_proof)
+        in
+        let sn = Seq_acc.take sub_stepno_seq in
+        Proof.T.Qed pf |> noprops |> with_stepno sn
+      in
+      Proof.T.(Steps ([ step_exists ], step_qed)) |> noprops
+    in
+    let step = Proof.T.Pick (bs, ex, step_pf) |> noprops in
+    [ (step_no, step) ] |> pp_proof_steps_before ps cx
+  in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx
+      (`Proof
+         Usable.(
+           empty |> add_steps (Seq_acc.acc step_names) |> add_to_pf ps_proof))
+  in
+  let title_ex = Expr.T.(Quant (Expr.T.Forall, bs, ex)) |> noprops in
+  let title =
+    Fmt.str "⤮ Use (∀): %a" (Debug.pp_expr_text (make_cx_hidden cx)) title_ex
+    |> limit_title
+  in
+  let ca =
+    ca_edits ~uri ~title ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+(** For each assumption in the form of existential quantifier,
+    {v
+      \E x \in X : P(x)
+    v}
+    and [pf] as the current proof, we introduce
+    {v
+      <1>a. PICK x \in X : P(x) [pf]
+    v} *)
+let cas_of_assm_exists (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    cx bs ex =
+  let open TL in
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let ps_proof = PS.proof ps |> Option.get in
+  let add_steps_rewrite =
+    let step_no = Seq_acc.take step_names in
+    let step = Proof.T.Pick (bs, ex, ps_proof) |> noprops in
+    [ (step_no, step) ] |> pp_proof_steps_before ps cx
+  in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx
+      (`Proof
+         Usable.(
+           empty |> add_steps (Seq_acc.acc step_names) |> add_to_pf ps_proof))
+  in
+  let title_ex = Expr.T.(Quant (Expr.T.Exists, bs, ex)) |> noprops in
+  let title =
+    Fmt.str "⤮ Use (∃): %a" (Debug.pp_expr_text (make_cx_hidden cx)) title_ex
+    |> limit_title
+  in
+  let ca =
+    ca_edits ~uri ~title ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+(** Match an assumption expression by its structure and propose the LSP Code
+    actions to decompose them. *)
+let cas_of_assm (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t) cx ex
+    =
+  let open TL in
+  let rec match_expr cx (ex : Expr.T.expr) =
+    match ex.core with
+    | Apply (op, op_args) -> (
+        match op.core with
+        | Internal bi -> (
+            match bi with
+            | Conj -> cas_of_assm_conj uri ps ps_parent cx op_args
+            | Disj -> cas_of_assm_disj uri ps ps_parent cx op_args
+            | Implies -> cas_of_assm_implies uri ps ps_parent cx op_args
+            | Equiv | TRUE | FALSE | Neg | Eq | Neq | STRING | BOOLEAN | SUBSET
+            | UNION | DOMAIN | Subseteq | Mem | Notmem | Setminus | Cap | Cup
+            | Prime | StrongPrime | Leadsto | ENABLED | UNCHANGED | Cdot
+            | Actplus | Box _ | Diamond | Nat | Int | Real | Plus | Minus
+            | Uminus | Times | Ratio | Quotient | Remainder | Exp | Infinity
+            | Lteq | Lt | Gteq | Gt | Divides | Range | Seq | Len | BSeq | Cat
+            | Append | Head | Tail | SubSeq | SelectSeq | OneArg | Extend
+            | Print | PrintT | Assert | JavaTime | TLCGet | TLCSet
+            | Permutations | SortSeq | RandomElement | Any | ToString
+            | Unprimable | Irregular ->
+                [])
+        | _ -> [])
+    | Quant (q, bs, e) -> (
+        match q with
+        | Forall -> cas_of_assm_forall uri ps ps_parent cx bs e
+        | Exists -> cas_of_assm_exists uri ps ps_parent cx bs e)
+    | List (bullet, exprs) -> (
+        match exprs with
+        | [] -> []
+        | [ expr ] -> match_expr cx expr
+        | _ :: _ -> (
+            match bullet with
+            | And | Refs -> cas_of_assm_conj uri ps ps_parent cx exprs
+            | Or -> cas_of_assm_disj uri ps ps_parent cx exprs))
+    | Sub (modal_op, action_ex, subscript_ex) ->
+        expand_sub modal_op action_ex subscript_ex |> match_expr cx
+    | Ix ix -> expand_expr_ref cx ix match_expr
+    | Opaque _ | Internal _
+    | Lambda (_, _)
+    | Sequent _
+    | Bang (_, _)
+    | With (_, _)
+    | If (_, _, _)
+    | Let (_, _)
+    | QuantTuply (_, _, _)
+    | Tquant (_, _, _)
+    | Choose (_, _, _)
+    | ChooseTuply (_, _, _)
+    | SetSt (_, _, _)
+    | SetStTuply (_, _, _)
+    | SetOf (_, _)
+    | SetOfTuply (_, _)
+    | SetEnum _ | Product _ | Tuple _
+    | Fcn (_, _)
+    | FcnTuply (_, _)
+    | FcnApp (_, _)
+    | Arrow (_, _)
+    | Rect _ | Record _
+    | Except (_, _)
+    | Dot (_, _)
+    | Tsub (_, _, _)
+    | Fair (_, _, _)
+    | Case (_, _)
+    | String _
+    | Num (_, _)
+    | At _
+    | Parens (_, _) ->
+        []
+  in
+  match_expr cx ex
+
+let code_actions (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    (cx : TL.Expr.T.ctx) =
+  let open TL in
+  let acc = ref [] in
+  let append add = acc := List.append !acc add in
+  let rec traverse_cx cx =
+    match Util.Deque.rear cx with
+    | None -> ()
+    | Some (cx, hyp) ->
+        (match hyp |> unwrap with
+        | Expr.T.Fresh (_, _, _, _)
+        | FreshTuply (_, _)
+        | Flex _
+        | Defn (_, _, _, _)
+        | Fact (_, Hidden, _) ->
+            ()
+        | Fact (ex, Visible, _) -> append (cas_of_assm uri ps ps_parent cx ex));
+        traverse_cx cx
+  in
+  traverse_cx cx;
+  !acc
diff --git a/lsp/lib/analysis/step_decompose/of_assm.mli b/lsp/lib/analysis/step_decompose/of_assm.mli
new file mode 100644
index 00000000..4dbf3d13
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/of_assm.mli
@@ -0,0 +1,9 @@
+module TL := Tlapm_lib
+module LspT := Util.LspT
+
+val code_actions :
+  Docs.tk ->
+  Docs.Proof_step.t ->
+  Docs.Proof_step.t ->
+  TL.Expr.T.ctx ->
+  LspT.CodeAction.t list
diff --git a/lsp/lib/analysis/step_decompose/of_defs.ml b/lsp/lib/analysis/step_decompose/of_defs.ml
new file mode 100644
index 00000000..9eaa5d27
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/of_defs.ml
@@ -0,0 +1,92 @@
+open Util
+
+(** List expandable names in the expression and its context. *)
+let expandable_names (cx : TL.Expr.T.ctx) (ex : TL.Expr.T.expr) : string list =
+  let open TL.Expr in
+  let names = ref StringSet.empty in
+  let add_name n = names := StringSet.add n !names in
+  let visitor =
+    object (_self : 'self)
+      inherit [unit] Visit.iter as super
+
+      method! expr (cx : unit Visit.scx) (e : T.expr) =
+        (match e.core with
+        | T.Opaque name -> add_name name
+        | T.Ix ix -> (
+            let hyp = T.get_val_from_id (snd cx) ix in
+            let cx = T.cx_front (snd cx) ix in
+            match hyp |> unwrap with
+            | T.Fresh (_, _, _, _) | T.FreshTuply (_, _) | T.Flex _ -> ()
+            | T.Defn (defn, _, T.Visible, _) ->
+                ignore (super#defn ((), cx) defn)
+            | T.Defn (_, _, T.Hidden, _) -> add_name (T.hyp_name hyp)
+            | T.Fact (ex, T.Visible, _) -> super#expr ((), cx) ex
+            | T.Fact (_, T.Hidden, _) -> ())
+        | T.Internal _
+        | T.Lambda (_, _)
+        | T.Sequent _
+        | T.Bang (_, _)
+        | T.Apply (_, _)
+        | T.With (_, _)
+        | T.If (_, _, _)
+        | T.List (_, _)
+        | T.Let (_, _)
+        | T.Quant (_, _, _)
+        | T.QuantTuply (_, _, _)
+        | T.Tquant (_, _, _)
+        | T.Choose (_, _, _)
+        | T.ChooseTuply (_, _, _)
+        | T.SetSt (_, _, _)
+        | T.SetStTuply (_, _, _)
+        | T.SetOf (_, _)
+        | T.SetOfTuply (_, _)
+        | T.SetEnum _ | T.Product _ | T.Tuple _
+        | T.Fcn (_, _)
+        | T.FcnTuply (_, _)
+        | T.FcnApp (_, _)
+        | T.Arrow (_, _)
+        | T.Rect _ | T.Record _
+        | T.Except (_, _)
+        | T.Dot (_, _)
+        | T.Sub (_, _, _)
+        | T.Tsub (_, _, _)
+        | T.Fair (_, _, _)
+        | T.Case (_, _)
+        | T.String _
+        | T.Num (_, _)
+        | T.At _
+        | T.Parens (_, _) ->
+            ());
+        super#expr cx e
+    end
+  in
+  let rec traverse_cx cx =
+    match TL.Util.Deque.rear cx with
+    | None -> ()
+    | Some (cx, hyp) ->
+        (match hyp |> unwrap with
+        | T.Fresh (_, _, _, _)
+        | T.FreshTuply (_, _)
+        | T.Flex _
+        | T.Defn (_, _, _, _)
+        | T.Fact (_, T.Hidden, _) ->
+            ()
+        | T.Fact (_, T.Visible, _) -> ignore (visitor#hyp ((), cx) hyp));
+        traverse_cx cx
+  in
+  visitor#expr ((), cx) ex;
+  traverse_cx cx;
+  StringSet.to_list !names |> List.sort String.compare
+
+(** Propose expand actions for all the definitions that are visible, but not yet
+    expanded.
+
+    TODO: "Expand all definitions"? *)
+let cas_def_expand ~uri ~(ps : PS.t) ~cx ~by ~(sq : TL.Expr.T.sequent) =
+  expandable_names sq.context sq.active
+  |> List.map @@ fun def_name ->
+     let usable, only = by in
+     let usable = usable |> Usable.add_defs_str [ def_name ] in
+     let new_pf = TL.Proof.T.By (usable, only) |> noprops in
+     let range, newText = ps_proof_rewrite ps cx (`Proof new_pf) in
+     ca_edit ~uri ~title:(Fmt.str "→ Expand %s" def_name) ~range ~newText
diff --git a/lsp/lib/analysis/step_decompose/of_defs.mli b/lsp/lib/analysis/step_decompose/of_defs.mli
new file mode 100644
index 00000000..dcf5c1b0
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/of_defs.mli
@@ -0,0 +1,10 @@
+module TL := Tlapm_lib
+module LspT := Util.LspT
+
+val cas_def_expand :
+  uri:Docs.tk ->
+  ps:Docs.Proof_step.t ->
+  cx:TL.Expr.T.hyp TL.Util.Deque.dq ->
+  by:TL.Proof.T.usable * bool ->
+  sq:TL.Expr.T.sequent ->
+  LspT.CodeAction.t list
diff --git a/lsp/lib/analysis/step_decompose/of_goal.ml b/lsp/lib/analysis/step_decompose/of_goal.ml
new file mode 100644
index 00000000..277af05f
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/of_goal.ml
@@ -0,0 +1,352 @@
+open Util
+
+(* Create code action for a goal in the form of implication. *)
+let cas_of_goal_implies (uri : LspT.DocumentUri.t) (ps : PS.t)
+    (ps_parent : PS.t) (cx : TL.Expr.T.ctx) (op_args : TL.Expr.T.expr list) =
+  let ps_proof = PS.proof ps |> Option.get in
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let antecedent = List.hd op_args in
+  let step = TL.Proof.T.Have antecedent |> noprops in
+  let step_no = Seq_acc.take step_names in
+  let title = "⤮ Decompose goal (⇒)" in
+  let add_steps_rewrite = [ (step_no, step) ] |> pp_proof_steps_before ps cx in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx
+      (`Usable
+         Usable.(
+           empty
+           |> add_steps (Seq_acc.acc step_names)
+           |> add_defs_from_pf ps_proof))
+  in
+  let ca =
+    ca_edits ~uri ~title ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+(** Create code action for a goal in the form of universal quantification. *)
+let cas_of_goal_forall (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    (cx : TL.Expr.T.ctx) (bs : TL.Expr.T.bound list) =
+  let title = "⤮ Decompose goal (∀)" in
+  let step = TL.Proof.T.Take bs |> noprops in
+  let edit =
+    [ (PS.sub_step_unnamed ps_parent, step) ] |> pp_proof_steps_before ps cx
+  in
+  let ca = ca_edits ~uri ~title ~edits:[ edit ] in
+  [ ca ]
+
+(** Create code action for a goal in the form of existential quantification.
+
+    {v
+      THEOREM TestGoalExists ==
+        ASSUME NEW P(_, _), NEW S
+        PROVE \E a, b \in S : P(a, b)
+      PROOF
+        \* <1> USE OBVIOUS
+        <1> DEFINE a == TRUE
+        <1> DEFINE b == TRUE
+        <1> HIDE DEF a, b
+        <1>1. a \in S
+        <1>2. b \in S
+        <1> WITNESS a \in S, b \in S
+        <1>3. QED OBVIOUS
+    v}
+
+    - For each bound, define a constant.
+    - Hide all defined constants.
+    - For each bound with a domain, introduce domain proof step.
+    - Then introduce the witness step. *)
+let cas_of_goal_exists (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    (cx : TL.Expr.T.ctx) (bs : TL.Expr.T.bound list) =
+  let title = "⤮ Decompose goal (∃)" in
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let bs_unditto = TL.Expr.T.unditto bs in
+  let fcx = fmt_cx cx in
+  let fresh_names = ref [] in
+  let steps_def =
+    bs
+    |> List.map @@ fun (b_name, _, _) ->
+       let fresh_var_name = fresh_ident fcx (unwrap b_name) in
+       fresh_names := fresh_var_name :: !fresh_names;
+       let step_no = PS.sub_step_unnamed ps_parent in
+       let step =
+         TL.Proof.T.Define
+           [
+             TL.Expr.T.Operator
+               ( b_name,
+                 TL.Expr.T.String
+                   (Fmt.str "TODO: Replace this with actual witness for %s"
+                      fresh_var_name)
+                 |> noprops )
+             |> noprops;
+           ]
+         |> noprops
+       in
+       (step_no, step)
+  in
+  let fresh_names = List.rev !fresh_names in
+  let step_hide =
+    let defs =
+      fresh_names |> List.map @@ fun name -> TL.Proof.T.Dvar name |> noprops
+    in
+    let step_no = PS.sub_step_unnamed ps_parent in
+    let step = TL.Proof.T.Hide { facts = []; defs } |> noprops in
+    (step_no, step)
+  in
+  let steps_pf_dom =
+    bs_unditto
+    |> ( List.mapi @@ fun pos (_, _, b_dom) ->
+         let fresh_name = List.nth fresh_names pos in
+         match b_dom with
+         | TL.Expr.T.Domain dom_expr ->
+             let active =
+               TL.Expr.T.Apply
+                 ( TL.Expr.T.Internal TL.Builtin.Mem |> noprops,
+                   [ TL.Expr.T.Opaque fresh_name |> noprops; dom_expr ] )
+               |> noprops
+             in
+             let step =
+               TL.Proof.T.Assert
+                 ( Sequent.of_goal active,
+                   TL.Proof.T.(Omitted Implicit) |> noprops )
+               |> noprops
+             in
+             let step_no = Seq_acc.take step_names in
+             Some (step_no, step)
+         | TL.Expr.T.No_domain | TL.Expr.T.Ditto -> None )
+    |> List.filter_map (fun x -> x)
+  in
+  let step_use =
+    Option.bind (PS.proof ps) @@ fun pf ->
+    match pf.core with
+    | TL.Proof.T.By (usable, only) ->
+        let step_no = Seq_acc.take step_names in
+        let step = TL.Proof.T.Use (usable, only) |> noprops in
+        Some (step_no, step)
+    | TL.Proof.T.Obvious | TL.Proof.T.Omitted _
+    | TL.Proof.T.Steps (_, _)
+    | TL.Proof.T.Error _ ->
+        None
+  in
+  let step_witness =
+    let exprs =
+      bs_unditto
+      |> List.mapi @@ fun pos (_, _, b_dom) ->
+         let fresh_name = List.nth fresh_names pos in
+         match b_dom with
+         | TL.Expr.T.No_domain | TL.Expr.T.Ditto ->
+             TL.Expr.T.Opaque fresh_name |> noprops
+         | TL.Expr.T.Domain dom ->
+             TL.Expr.T.Apply
+               ( TL.Expr.T.Internal TL.Builtin.Mem |> noprops,
+                 [ TL.Expr.T.Opaque fresh_name |> noprops; dom ] )
+             |> noprops
+    in
+    let step = TL.Proof.T.Witness exprs |> noprops in
+    let step_no = PS.sub_step_unnamed ps_parent in
+    (step_no, step)
+  in
+  let edit =
+    List.concat
+      [
+        steps_def;
+        [ step_hide ];
+        steps_pf_dom;
+        Option.to_list step_use;
+        [ step_witness ];
+      ]
+    |> pp_proof_steps_before ps cx
+  in
+  let ca = ca_edits ~uri ~title ~edits:[ edit ] in
+  [ ca ]
+
+(** Create a code action for a goal in the form of conjunction. *)
+let cas_of_goal_conj (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    cx op_args =
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let ps_proof = PS.proof ps |> Option.get in
+  let add_steps_rewrite =
+    flatten_op_list Conj op_args
+    |> List.map (fun op ->
+        let step_no = Seq_acc.take step_names in
+        let step =
+          TL.Proof.T.Assert (Sequent.of_goal op, ps_proof) |> noprops
+        in
+        (step_no, step))
+    |> pp_proof_steps_before ps cx
+  in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx
+      (`Usable
+         Usable.(
+           empty
+           |> add_steps (Seq_acc.acc step_names)
+           |> add_defs_from_pf ps_proof))
+  in
+  let ca =
+    ca_edits ~uri ~title:"⤮ Decompose goal (∧)"
+      ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+(** Make decomposition code actions for a goal of the form of disjunction. In
+    general we leave one disjunct as a goal and assume all the rest are negated.
+    - We don't know which one to pick, thus propose user all of them.
+    - The current step proof is then replaced with the BY <x>y referring to the
+      introduced SUFFICES. *)
+let cas_of_goal_disj (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    cx disjuncts =
+  let disjuncts = flatten_op_list Disj disjuncts in
+  let ps_proof = PS.proof ps |> Option.get in
+  let disjunct_ca disjunct_pos disjunct =
+    let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+    let step_no = Seq_acc.take step_names in
+    let other_negated =
+      disjuncts
+      |> List.filteri (fun i _ -> i != disjunct_pos)
+      |> List.mapi (fun i disjunct ->
+          (* TODO: Drop existing negation, if there exist instead of adding yet another. *)
+          let expr =
+            TL.Expr.T.Apply
+              (TL.(Expr.T.Internal Builtin.Neg) |> noprops, [ disjunct ])
+            |> noprops
+          in
+          TL.Expr.T.(Fact (expr, Visible, NotSet))
+          |> noprops
+          |> TL.Expr.Subst.(app_hyp (shift i)))
+    in
+    let disjunct =
+      disjunct |> TL.Expr.Subst.(app_expr (shift (List.length other_negated)))
+    in
+    let step =
+      TL.Proof.T.Suffices
+        ( { context = TL.Util.Deque.of_list other_negated; active = disjunct },
+          ps_proof )
+      |> noprops
+    in
+    let new_step_rewrite = pp_proof_steps_before ps cx [ (step_no, step) ] in
+    let ps_proof_rewrite = ps_proof_rewrite ps cx (`StepNames [ step_no ]) in
+    ca_edits ~uri
+      ~title:(Fmt.str "⤮ Decompose goal (∨, case %d)" (disjunct_pos + 1))
+      ~edits:[ new_step_rewrite; ps_proof_rewrite ]
+  in
+  List.mapi disjunct_ca disjuncts
+
+(* A chain of equivalences is replaced with a list of circular implications. *)
+let cas_of_goal_equiv (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    cx op_args =
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps_parent) in
+  let add_steps_rewrite =
+    let ps_proof = PS.proof ps |> Option.get in
+    let op_args = flatten_op_list Equiv op_args in
+    let next_arg i = List.nth op_args ((i + 1) mod List.length op_args) in
+    op_args
+    |> List.mapi (fun i op ->
+        let step_no = Seq_acc.take step_names in
+        let step_goal =
+          TL.Expr.T.Apply
+            ( TL.Expr.T.Internal TL.Builtin.Implies |> noprops,
+              [ op; next_arg i ] )
+          |> noprops
+        in
+        let step =
+          TL.Proof.T.Assert (Sequent.of_goal step_goal, ps_proof) |> noprops
+        in
+        (step_no, step))
+    |> pp_proof_steps_before ps cx
+  in
+  let ps_proof_rewrite =
+    ps_proof_rewrite ps cx (`StepNames (Seq_acc.acc step_names))
+  in
+  let ca =
+    ca_edits ~uri ~title:"⤮ Decompose goal (≡)"
+      ~edits:[ add_steps_rewrite; ps_proof_rewrite ]
+  in
+  [ ca ]
+
+let code_actions (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    (sq : TL.Expr.T.sequent) =
+  let rec match_expr cx (ex : TL.Expr.T.expr) =
+    match ex.core with
+    | TL.Expr.T.Apply (op, op_args) -> (
+        match op.core with
+        | TL.Expr.T.Internal bi -> (
+            match bi with
+            | TL.Builtin.Implies ->
+                cas_of_goal_implies uri ps ps_parent cx op_args
+            | TL.Builtin.Conj -> cas_of_goal_conj uri ps ps_parent cx op_args
+            | TL.Builtin.Disj -> cas_of_goal_disj uri ps ps_parent cx op_args
+            | TL.Builtin.Equiv -> cas_of_goal_equiv uri ps ps_parent cx op_args
+            | TL.Builtin.TRUE | TL.Builtin.FALSE | TL.Builtin.Neg
+            | TL.Builtin.Eq | TL.Builtin.Neq | TL.Builtin.STRING
+            | TL.Builtin.BOOLEAN | TL.Builtin.SUBSET | TL.Builtin.UNION
+            | TL.Builtin.DOMAIN | TL.Builtin.Subseteq | TL.Builtin.Mem
+            | TL.Builtin.Notmem | TL.Builtin.Setminus | TL.Builtin.Cap
+            | TL.Builtin.Cup | TL.Builtin.Prime | TL.Builtin.StrongPrime
+            | TL.Builtin.Leadsto | TL.Builtin.ENABLED | TL.Builtin.UNCHANGED
+            | TL.Builtin.Cdot | TL.Builtin.Actplus | TL.Builtin.Box _
+            | TL.Builtin.Diamond | TL.Builtin.Nat | TL.Builtin.Int
+            | TL.Builtin.Real | TL.Builtin.Plus | TL.Builtin.Minus
+            | TL.Builtin.Uminus | TL.Builtin.Times | TL.Builtin.Ratio
+            | TL.Builtin.Quotient | TL.Builtin.Remainder | TL.Builtin.Exp
+            | TL.Builtin.Infinity | TL.Builtin.Lteq | TL.Builtin.Lt
+            | TL.Builtin.Gteq | TL.Builtin.Gt | TL.Builtin.Divides
+            | TL.Builtin.Range | TL.Builtin.Seq | TL.Builtin.Len
+            | TL.Builtin.BSeq | TL.Builtin.Cat | TL.Builtin.Append
+            | TL.Builtin.Head | TL.Builtin.Tail | TL.Builtin.SubSeq
+            | TL.Builtin.SelectSeq | TL.Builtin.OneArg | TL.Builtin.Extend
+            | TL.Builtin.Print | TL.Builtin.PrintT | TL.Builtin.Assert
+            | TL.Builtin.JavaTime | TL.Builtin.TLCGet | TL.Builtin.TLCSet
+            | TL.Builtin.Permutations | TL.Builtin.SortSeq
+            | TL.Builtin.RandomElement | TL.Builtin.Any | TL.Builtin.ToString
+            | TL.Builtin.Unprimable | TL.Builtin.Irregular ->
+                [])
+        | _ -> [])
+    | TL.Expr.T.Quant (q, bs, _e) -> (
+        match q with
+        | TL.Expr.T.Forall -> cas_of_goal_forall uri ps ps_parent cx bs
+        | TL.Expr.T.Exists -> cas_of_goal_exists uri ps ps_parent cx bs)
+    | TL.Expr.T.List (bullet, exprs) -> (
+        match exprs with
+        | [] -> []
+        | [ expr ] -> match_expr cx expr
+        | _ :: _ -> (
+            match bullet with
+            | TL.Expr.T.And | TL.Expr.T.Refs ->
+                cas_of_goal_conj uri ps ps_parent cx exprs
+            | TL.Expr.T.Or -> cas_of_goal_disj uri ps ps_parent cx exprs))
+    | TL.Expr.T.Sub (modal_op, action_ex, subscript_ex) ->
+        expand_sub modal_op action_ex subscript_ex |> match_expr cx
+    | TL.Expr.T.Ix ix -> expand_expr_ref cx ix match_expr
+    | TL.Expr.T.Opaque _ | TL.Expr.T.Internal _
+    | TL.Expr.T.Lambda (_, _)
+    | TL.Expr.T.Sequent _
+    | TL.Expr.T.Bang (_, _)
+    | TL.Expr.T.With (_, _)
+    | TL.Expr.T.If (_, _, _)
+    | TL.Expr.T.Let (_, _)
+    | TL.Expr.T.QuantTuply (_, _, _)
+    | TL.Expr.T.Tquant (_, _, _)
+    | TL.Expr.T.Choose (_, _, _)
+    | TL.Expr.T.ChooseTuply (_, _, _)
+    | TL.Expr.T.SetSt (_, _, _)
+    | TL.Expr.T.SetStTuply (_, _, _)
+    | TL.Expr.T.SetOf (_, _)
+    | TL.Expr.T.SetOfTuply (_, _)
+    | TL.Expr.T.SetEnum _ | TL.Expr.T.Product _ | TL.Expr.T.Tuple _
+    | TL.Expr.T.Fcn (_, _)
+    | TL.Expr.T.FcnTuply (_, _)
+    | TL.Expr.T.FcnApp (_, _)
+    | TL.Expr.T.Arrow (_, _)
+    | TL.Expr.T.Rect _ | TL.Expr.T.Record _
+    | TL.Expr.T.Except (_, _)
+    | TL.Expr.T.Dot (_, _)
+    | TL.Expr.T.Tsub (_, _, _)
+    | TL.Expr.T.Fair (_, _, _)
+    | TL.Expr.T.Case (_, _)
+    | TL.Expr.T.String _
+    | TL.Expr.T.Num (_, _)
+    | TL.Expr.T.At _
+    | TL.Expr.T.Parens (_, _) ->
+        []
+  in
+  match_expr sq.context sq.active
diff --git a/lsp/lib/analysis/step_decompose/of_goal.mli b/lsp/lib/analysis/step_decompose/of_goal.mli
new file mode 100644
index 00000000..2f4d68c0
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/of_goal.mli
@@ -0,0 +1,9 @@
+module TL := Tlapm_lib
+module LspT := Util.LspT
+
+val code_actions :
+  Docs.tk ->
+  Docs.Proof_step.t ->
+  Docs.Proof_step.t ->
+  TL.Expr.T.sequent ->
+  LspT.CodeAction.t list
diff --git a/lsp/lib/analysis/step_decompose/sequent.ml b/lsp/lib/analysis/step_decompose/sequent.ml
new file mode 100644
index 00000000..e5d0a90a
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/sequent.ml
@@ -0,0 +1,4 @@
+module TL = Tlapm_lib
+
+let of_goal (ex : TL.Expr.T.expr) : TL.Expr.T.sequent =
+  { context = TL.Util.Deque.empty; active = ex }
diff --git a/lsp/lib/analysis/step_decompose/step_decompose.ml b/lsp/lib/analysis/step_decompose/step_decompose.ml
new file mode 100644
index 00000000..6528c1d0
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/step_decompose.ml
@@ -0,0 +1,113 @@
+(* cspell:words Actplus Cdot Deque Disj Forall Gteq Leadsto Lteq Notmem Setminus Tquant unditto *)
+(* cspell:words Tquant Tsub Uminus Unprimable noprops stepno uncons Bpragma Defn  Dvar  assm  filteri *)
+open Util
+
+(** Replace
+    {v <1> ... v}
+    with
+    {v <1> ... OBVIOUS v} *)
+let ca_omitted ~uri ~ps =
+  let title = "⤮ Prove as OBVIOUS" in
+  let range = PS.head_range ps |> Range.make_after in
+  let newText = " OBVIOUS" in
+  ca_edit ~uri ~title ~range ~newText
+
+(** Replace
+    {v
+      <1> ... [proof]
+    v}
+    with
+    {v
+      <1> ...
+        <2>1. QED [proof]
+    v} *)
+let ca_to_steps ~uri ~(ps : PS.t) ~cx =
+  let open TL in
+  let step_names = Seq_acc.make (PS.stepno_seq_under_proof_step ps) in
+  let ps_proof = PS.proof ps |> Option.get in
+  let sub_steps =
+    let qed_sn = Seq_acc.take step_names in
+    let qed = Proof.T.Qed ps_proof |> noprops |> with_stepno qed_sn in
+    Proof.T.(Steps ([], qed)) |> noprops
+  in
+  let ps_proof_rewrite = ps_proof_rewrite ps cx (`Proof sub_steps) in
+  let title = "⤮ To sub-steps" in
+  ca_edits ~uri ~title ~edits:[ ps_proof_rewrite ]
+
+(* Propose code actions for AST nodes containing proofs. *)
+let cas_of_el_with_pf (uri : LspT.DocumentUri.t) (ps : PS.t)
+    (cx : TL.Expr.T.ctx) (pf : TL.Proof.T.proof) =
+  let cas_def_expand (by : (TL.Proof.T.usable * bool) option) =
+    let by =
+      Option.value ~default:(TL.Proof.T.{ facts = []; defs = [] }, false) by
+    in
+    PS.goal ps
+    |> Option.fold ~none:[] ~some:(fun g ->
+        Of_defs.cas_def_expand ~uri ~ps ~cx ~by ~sq:TL.Proof.T.(g.obl |> unwrap))
+  in
+  let open TL.Proof.T in
+  match unwrap pf with
+  | Omitted Implicit ->
+      List.concat
+        [
+          [ ca_omitted ~uri ~ps; ca_to_steps ~uri ~ps ~cx ]; cas_def_expand None;
+        ]
+  | Omitted Explicit | Omitted (Elsewhere _) ->
+      List.concat [ [ ca_to_steps ~uri ~ps ~cx ]; cas_def_expand None ]
+  | Steps ([], _) ->
+      (* TODO: Drop one level. *)
+      []
+  | Steps (_, _) -> []
+  | Obvious -> List.concat [ [ ca_to_steps ~uri ~ps ~cx ]; cas_def_expand None ]
+  | By (usable, only) ->
+      List.concat
+        [ [ ca_to_steps ~uri ~ps ~cx ]; cas_def_expand (Some (usable, only)) ]
+  | Error _ -> []
+
+(** Propose proof decomposition CodeActions by the structure of the goal and
+    assumptions. *)
+let cas_of_obl (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t)
+    (o : TL.Proof.T.obligation) =
+  let o = TL.Backend.Toolbox.normalize true o in
+  List.concat
+    [
+      Of_goal.code_actions uri ps ps_parent o.obl.core;
+      Of_assm.code_actions uri ps ps_parent o.obl.core.context;
+    ]
+
+(* Code Actions of Proof Step *)
+let cas_of_ps (uri : LspT.DocumentUri.t) (ps : PS.t) (ps_parent : PS.t) =
+  let open TL.Proof.T in
+  let el, cx = PS.el ps in
+  let cas_of_el_with_pf = cas_of_el_with_pf uri ps cx in
+  match el with
+  | PS.El.Mutate _ | PS.El.Module _ -> []
+  | PS.El.Theorem { orig_pf; _ } -> cas_of_el_with_pf orig_pf
+  | PS.El.Step step -> (
+      match unwrap step with
+      | Assert (_, pf)
+      | Suffices (_, pf)
+      | Pcase (_, pf)
+      | Pick (_, _, pf)
+      | PickTuply (_, _, pf) ->
+          cas_of_el_with_pf pf
+      | Hide _ | Define _
+      | Use (_, _)
+      | Have _ | Take _ | TakeTuply _ | Witness _ | Forget _ ->
+          [])
+  | PS.El.Qed qed_step ->
+      let cas_of_goal =
+        PS.goal ps
+        |> Option.fold ~none:[] ~some:(fun g -> cas_of_obl uri ps ps_parent g)
+      in
+      let cas_of_pf =
+        match unwrap qed_step with Qed pf -> cas_of_el_with_pf pf
+      in
+      List.concat [ cas_of_goal; cas_of_pf ]
+
+let code_actions (uri : LspT.DocumentUri.t) (mule_ps : PS.t) (range : Range.t) :
+    LspT.CodeAction.t list =
+  match PS.locate_proof_path mule_ps range with
+  | ps :: parent :: _ -> cas_of_ps uri ps parent
+  | _ :: _ -> [] (* Module is the root, no decompositions there. *)
+  | [] -> [] (* Should not be possible. *)
diff --git a/lsp/lib/analysis/step_decompose/step_decompose.mli b/lsp/lib/analysis/step_decompose/step_decompose.mli
new file mode 100644
index 00000000..85b1a876
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/step_decompose.mli
@@ -0,0 +1,5 @@
+(* https://github.com/tlaplus/tlaplus/blob/master/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/handlers/DecomposeProofHandler.java *)
+module LspT := Lsp.Types
+
+val code_actions :
+  LspT.DocumentUri.t -> Docs.Proof_step.t -> Range.t -> LspT.CodeAction.t list
diff --git a/lsp/lib/analysis/step_decompose/usable.ml b/lsp/lib/analysis/step_decompose/usable.ml
new file mode 100644
index 00000000..b1005ca2
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/usable.ml
@@ -0,0 +1,46 @@
+module TL = Tlapm_lib
+open TL.Proof.T
+open TL.Expr.T
+
+let noprops = TL.Property.noprops
+
+(** Usable, but cannot be used if left empty. *)
+let empty : usable = { facts = []; defs = [] }
+
+let add_steps (step_names : stepno list) (usable : usable) : usable =
+  let new_facts =
+    List.map (fun sn -> Opaque (string_of_stepno sn) |> noprops) step_names
+  in
+  { usable with facts = List.append usable.facts new_facts }
+
+let add_defs new_defs usable : usable =
+  { usable with defs = List.append usable.defs new_defs }
+
+let add_defs_str def_names usable : usable =
+  let new_defs =
+    def_names |> List.map @@ fun def_name -> Dvar def_name |> noprops
+  in
+  add_defs new_defs usable
+
+let add_defs_from_pf (pf : proof) usable : usable =
+  match pf.core with
+  | By ({ defs; _ }, _) -> { usable with defs = List.append usable.defs defs }
+  | Obvious | Omitted _ | Steps (_, _) | Error _ -> usable
+
+let rec add_to_pf (pf : proof) (u : usable) : proof =
+  match pf.core with
+  | Obvious | Omitted _ -> TL.Property.(By (u, false) @@ pf)
+  | By ({ facts; defs }, only) ->
+      let u =
+        { facts = List.append facts u.facts; defs = List.append defs u.defs }
+      in
+      TL.Property.(By (u, only) @@ pf)
+  | Steps (steps, qed) ->
+      let qed =
+        match qed.core with
+        | Qed qed_pf ->
+            let qed_pf = add_to_pf qed_pf u in
+            TL.Property.(Qed qed_pf @@ qed)
+      in
+      TL.Property.(Steps (steps, qed) @@ pf)
+  | Error _ -> pf
diff --git a/lsp/lib/analysis/step_decompose/usable.mli b/lsp/lib/analysis/step_decompose/usable.mli
new file mode 100644
index 00000000..f74b40be
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/usable.mli
@@ -0,0 +1,19 @@
+(** Helpers for working with [TL.Proof.T.usable]. *)
+
+module TL := Tlapm_lib
+
+val empty : TL.Proof.T.usable
+val add_steps : TL.Proof.T.stepno list -> TL.Proof.T.usable -> TL.Proof.T.usable
+
+val add_defs :
+  TL.Proof.T.use_def TL.Property.wrapped list ->
+  TL.Proof.T.usable ->
+  TL.Proof.T.usable
+
+val add_defs_str : string list -> TL.Proof.T.usable -> TL.Proof.T.usable
+
+val add_defs_from_pf :
+  TL.Proof.T.proof -> TL.Proof.T.usable -> TL.Proof.T.usable
+
+val add_to_pf : TL.Proof.T.proof -> TL.Proof.T.usable -> TL.Proof.T.proof
+(** Merge usable into an existing proof. *)
diff --git a/lsp/lib/analysis/step_decompose/util.ml b/lsp/lib/analysis/step_decompose/util.ml
new file mode 100644
index 00000000..eb406aa4
--- /dev/null
+++ b/lsp/lib/analysis/step_decompose/util.ml
@@ -0,0 +1,226 @@
+module PS = Docs.Proof_step
+module TL = Tlapm_lib
+module LspT = Lsp.Types
+module StringSet = Set.Make (String)
+
+let noprops = TL.Property.noprops
+let unwrap = TL.Property.unwrap
+let with_stepno sn w = TL.Property.with_prop TL.Proof.T.Props.step sn w
+
+let expand_expr_ref cx ix f =
+  let hyp = TL.Expr.T.get_val_from_id cx ix in
+  let cx = TL.Expr.T.cx_front cx ix in
+  match hyp.core with
+  | TL.Expr.T.Fresh (_, _, _, _)
+  | TL.Expr.T.FreshTuply (_, _)
+  | TL.Expr.T.Flex _ ->
+      []
+  | TL.Expr.T.Defn (defn, _, Visible, _) -> (
+      match defn.core with
+      | TL.Expr.T.Operator (_, ex) -> f cx ex
+      | TL.Expr.T.Recursive (_, _)
+      | TL.Expr.T.Instance (_, _)
+      | TL.Expr.T.Bpragma (_, _, _) ->
+          [])
+  | TL.Expr.T.Defn (_, _, _, _) -> []
+  | TL.Expr.T.Fact (ex, Visible, _) -> f cx ex
+  | TL.Expr.T.Fact (_, _, _) -> []
+
+let join_exs ~unit ~op exs =
+  let open TL.Expr.T in
+  let ex =
+    exs
+    |> List.fold_left
+         (fun acc ex ->
+           match acc with
+           | None -> Some ex
+           | Some acc -> Some (Apply (op, [ acc; ex ]) |> noprops))
+         None
+  in
+  Option.value ~default:unit ex
+
+let make_disjunction exs =
+  let open TL.Expr.T in
+  let open TL.Builtin in
+  join_exs ~unit:(Internal FALSE |> noprops) ~op:(Internal Disj |> noprops) exs
+
+let make_conjunction exs =
+  let open TL.Expr.T in
+  let open TL.Builtin in
+  join_exs ~unit:(Internal TRUE |> noprops) ~op:(Internal Conj |> noprops) exs
+
+let expand_sub modal_op action_ex subscript_ex =
+  let open TL.Expr.T in
+  let open TL.Builtin in
+  let unchanged =
+    Apply (Internal UNCHANGED |> noprops, [ subscript_ex ]) |> noprops
+  in
+  match modal_op with
+  | TL.Expr.T.Box -> make_disjunction [ action_ex; unchanged ]
+  | TL.Expr.T.Dia ->
+      let changed = Apply (Internal Neg |> noprops, [ unchanged ]) |> noprops in
+      make_conjunction [ action_ex; changed ]
+
+type flatten_by = Conj | Disj | Equiv | Implies
+
+let rec flatten_op_list (by : flatten_by) (exs : TL.Expr.T.expr list) :
+    TL.Expr.T.expr list =
+  exs |> List.map (fun arg -> flatten_op by arg) |> List.flatten
+
+and flatten_op (by : flatten_by) (ex : TL.Expr.T.expr) : TL.Expr.T.expr list =
+  let open TL.Expr.T in
+  let open TL.Builtin in
+  match ex.core with
+  | Apply (op, args) -> (
+      match op.core with
+      | Internal bi -> (
+          match bi with
+          | Conj when by = Conj -> flatten_op_list by args
+          | Disj when by = Disj -> flatten_op_list by args
+          | Equiv when by = Equiv -> flatten_op_list by args
+          | Implies when by = Implies -> flatten_op_list by args
+          | _ -> [ ex ])
+      | _ -> [ ex ])
+  | List (bullet, list) -> (
+      match bullet with
+      | And when by = Conj -> flatten_op_list by list
+      | Refs when by = Conj -> flatten_op_list by list
+      | Or when by = Disj -> flatten_op_list by list
+      | _ -> [ ex ])
+  | Sub (modal_op, action_ex, subscript_ex) -> (
+      match modal_op with
+      | Box when by = Disj ->
+          flatten_op_list by [ expand_sub modal_op action_ex subscript_ex ]
+      | Dia when by = Conj ->
+          flatten_op_list by [ expand_sub modal_op action_ex subscript_ex ]
+      | _ -> [ ex ])
+  | _ -> [ ex ]
+
+(* Helpers for formatting the TLA code. *)
+
+(* TODO: A hacked-up approach to indentation. *)
+let indent (ps : PS.t) ~nested text =
+  let nested = if nested then 2 else 0 in
+  let _line, char = PS.full_range ps |> Range.from |> Range.Position.as_pair in
+  let indent =
+    Array.make (char - 1 + nested) ' ' |> Array.to_seq |> String.of_seq
+  in
+  let template = String.cat "\n" indent in
+  Re2.rewrite_exn (Re2.create_exn "\n") ~template text
+
+let indent_size (ps : PS.t) ~nested =
+  let nested = if nested then 2 else 0 in
+  let _line, char = PS.full_range ps |> Range.from |> Range.Position.as_pair in
+  char - 1 + nested
+
+let fmt_cx cx =
+  let fcx = TL.Ctx.dot |> TL.Ctx.with_try_print_src in
+  let fcx =
+    (* Push all the names known in the context to have proper
+    suffixes _1, _2, ... for newly introduced identifiers. *)
+    TL.Util.Deque.fold_left
+      (fun fcx (hyp : TL.Expr.T.hyp) ->
+        match hyp.core with
+        | TL.Expr.T.Flex name | TL.Expr.T.Fresh (name, _, _, _) ->
+            TL.Ctx.push fcx (unwrap name)
+        | TL.Expr.T.FreshTuply (names, _) ->
+            List.fold_right
+              (fun name fcx -> TL.Ctx.push fcx (unwrap name))
+              names fcx
+        | TL.Expr.T.Defn (defn, _, _, _) -> (
+            match defn.core with
+            | TL.Expr.T.Recursive (name, _)
+            | TL.Expr.T.Operator (name, _)
+            | TL.Expr.T.Instance (name, _)
+            | TL.Expr.T.Bpragma (name, _, _) ->
+                TL.Ctx.push fcx (unwrap name))
+        | TL.Expr.T.Fact (_, _, _) -> TL.Ctx.bump fcx)
+      fcx cx
+  in
+  (cx, fcx)
+
+let pp_proof cx fmt st = ignore (TL.Proof.Fmt.pp_print_proof (fmt_cx cx) fmt st)
+
+let pp_proof_step cx fmt st =
+  ignore (TL.Proof.Fmt.pp_print_step (fmt_cx cx) fmt st)
+
+let pp_proof_step_no fmt (sn : TL.Proof.T.stepno) =
+  let str = TL.Proof.T.string_of_stepno sn in
+  match sn with
+  | TL.Proof.T.Named (_, _, _) -> Fmt.pf fmt "%s." str
+  | TL.Proof.T.Unnamed (_, _) -> Fmt.pf fmt "%s" str
+
+let pp_proof_step_with_no cx fmt (step_no, step) =
+  Fmt.pf fmt "@[%a @[%a@]@]" pp_proof_step_no step_no (pp_proof_step cx) step
+
+let pp_proof_step_list ps cx steps =
+  let indent = indent_size ps ~nested:false in
+  Fmt.str "@[<v %d>%s%a@]@." indent (String.make indent ' ')
+    (Fmt.list ~sep:Format.pp_force_newline (pp_proof_step_with_no cx))
+    steps
+
+let pp_proof_steps_before ps cx steps =
+  let range = Range.make_before_ln (PS.full_range ps) in
+  let text = pp_proof_step_list ps cx steps in
+  (range, text)
+
+(** Creates a rewrite for the proof of the current step, replacing it with BY
+    and the step names listed. *)
+let ps_proof_rewrite ps cx step_info =
+  let r =
+    Range.of_points
+      (Range.from (PS.head_range ps |> Range.make_after))
+      (Range.till (PS.full_range ps |> Range.with_end_line))
+  in
+  let ps_proof_new =
+    match step_info with
+    | `StepNames step_names ->
+        TL.Proof.T.By
+          ( {
+              facts =
+                List.map
+                  (fun sn ->
+                    TL.Expr.T.Opaque (TL.Proof.T.string_of_stepno sn) |> noprops)
+                  step_names;
+              defs = [];
+            },
+            false )
+        |> noprops
+    | `Usable us -> TL.Proof.T.By (us, false) |> noprops
+    | `Proof pf -> pf
+  in
+  let t =
+    match ps_proof_new.core with
+    | Obvious | Omitted _ | By (_, _) | Error _ ->
+        Fmt.str "@[@ %a@]@." (pp_proof cx) ps_proof_new
+    | Steps (_, _) ->
+        let indent = indent_size ps ~nested:true in
+        Fmt.str "@.@[<v %d>%s%a@]@." indent (String.make indent ' ')
+          (pp_proof cx) ps_proof_new
+  in
+  (r, t)
+
+(** Produce new unique name in the context (can be obtained by calling fmt_cx).
+    The argument [name] is a base for generating the identifier. It might be
+    returned as is, of suffixed with some number. *)
+let fresh_ident (fmt_cx : TL.Expr.T.ctx * int TL.Ctx.ctx) (name : string) :
+    string =
+  let _ecx, fcx = fmt_cx in
+  TL.Ctx.push fcx name |> TL.Ctx.front |> TL.Ctx.string_of_ident
+
+(** {1 Helpers for constructing code actions.} *)
+
+let ca_edit ~uri ~title ~range ~newText =
+  let edit = LspT.TextEdit.create ~newText ~range:(Range.as_lsp_range range) in
+  let edit = LspT.WorkspaceEdit.create ~changes:[ (uri, [ edit ]) ] () in
+  LspT.CodeAction.create ~title ~edit ~kind:LspT.CodeActionKind.Refactor ()
+
+let ca_edits ~uri ~title ~edits =
+  let edits =
+    List.map
+      (fun (r, t) ->
+        LspT.TextEdit.create ~newText:t ~range:(Range.as_lsp_range r))
+      edits
+  in
+  let edit = LspT.WorkspaceEdit.create ~changes:[ (uri, edits) ] () in
+  LspT.CodeAction.create ~title ~edit ()
diff --git a/lsp/lib/debug.ml b/lsp/lib/debug.ml
index de8435ff..e7596add 100644
--- a/lsp/lib/debug.ml
+++ b/lsp/lib/debug.ml
@@ -1,3 +1,5 @@
+let unwrap = Tlapm_lib.Property.unwrap
+
 class visitor_pp =
   object (self)
     val mutable acc : (Format.formatter -> unit) list = []
@@ -48,6 +50,22 @@ class visitor_pp =
       fun name f -> self#scope (Format.dprintf "%s{%t}" name) f
   end
 
+let pp_visibility fmt (v : Tlapm_lib.Expr.T.visibility) =
+  match v with
+  | Tlapm_lib.Expr.T.Visible -> Fmt.pf fmt "Visible"
+  | Tlapm_lib.Expr.T.Hidden -> Fmt.pf fmt "Hidden"
+
+let pp_bullet fmt (v : Tlapm_lib.Expr.T.bullet) =
+  match v with
+  | Tlapm_lib.Expr.T.And -> Fmt.pf fmt "And"
+  | Tlapm_lib.Expr.T.Or -> Fmt.pf fmt "Or"
+  | Tlapm_lib.Expr.T.Refs -> Fmt.pf fmt "Refs"
+
+let pp_expr_text cx fmt expr =
+  Fmt.pf fmt "@[%a@]"
+    (Tlapm_lib.Expr.Fmt.pp_print_expr (cx, Tlapm_lib.Ctx.dot))
+    expr
+
 let pp_expr (fmt : Format.formatter) (expr : Tlapm_lib.Expr.T.expr) : unit =
   let open Tlapm_lib.Expr.T in
   match expr.core with
@@ -61,7 +79,8 @@ let pp_expr (fmt : Format.formatter) (expr : Tlapm_lib.Expr.T.expr) : unit =
   | Apply (_, _) -> Format.fprintf fmt "Apply"
   | With (_, _) -> Format.fprintf fmt "With"
   | If (_, _, _) -> Format.fprintf fmt "If"
-  | List (_, _) -> Format.fprintf fmt "List"
+  | List (b, exs) ->
+      Format.fprintf fmt "List/%d-%a" (List.length exs) pp_bullet b
   | Let (_, _) -> Format.fprintf fmt "Let"
   | Quant (_, _, _) -> Format.fprintf fmt "Quant"
   | QuantTuply (_, _, _) -> Format.fprintf fmt "QuantTuply"
@@ -92,6 +111,34 @@ let pp_expr (fmt : Format.formatter) (expr : Tlapm_lib.Expr.T.expr) : unit =
   | At _ -> Format.fprintf fmt "At"
   | Parens (_, _) -> Format.fprintf fmt "Parens"
 
+let pp_defn (fmt : Format.formatter) (defn : Tlapm_lib.Expr.T.defn) : unit =
+  match defn.core with
+  | Tlapm_lib.Expr.T.Recursive (n, _) ->
+      Format.fprintf fmt "Recursive %s" (unwrap n)
+  | Tlapm_lib.Expr.T.Operator (n, _) ->
+      Format.fprintf fmt "Operator %s" (unwrap n)
+  | Tlapm_lib.Expr.T.Instance (n, _) ->
+      Format.fprintf fmt "Instance %s" (unwrap n)
+  | Tlapm_lib.Expr.T.Bpragma (n, _, _) ->
+      Format.fprintf fmt "Bpragma %s" (unwrap n)
+
+let pp_hyp (fmt : Format.formatter) (hyp : Tlapm_lib.Expr.T.hyp) : unit =
+  match hyp.core with
+  | Tlapm_lib.Expr.T.Fresh (hint, _, _, _) ->
+      Format.fprintf fmt "Fresh %s" (unwrap hint)
+  | Tlapm_lib.Expr.T.FreshTuply (_, _) -> Format.fprintf fmt "FreshTuply"
+  | Tlapm_lib.Expr.T.Flex hint -> Format.fprintf fmt "Flex %s" (unwrap hint)
+  | Tlapm_lib.Expr.T.Defn (defn, _, _, _) ->
+      Format.fprintf fmt "Defn %a" pp_defn defn
+  | Tlapm_lib.Expr.T.Fact (expr, visible, _) ->
+      Format.fprintf fmt "@[Fact/%a %a@]" pp_visibility visible pp_expr expr
+
+let pp_cx (fmt : Format.formatter)
+    (cx : Tlapm_lib.Expr.T.hyp Tlapm_lib.Util.Deque.dq) : unit =
+  Fmt.pf fmt "@[%a@]"
+    (Fmt.list ~sep:Format.pp_force_newline pp_hyp)
+    (Tlapm_lib.Util.Deque.to_list cx)
+
 let%test_unit "example use of visitor_pp" =
   let filename = "test_obl_expand.tla" in
   let content =
diff --git a/lsp/lib/debug.mli b/lsp/lib/debug.mli
index 1f63c63c..a01c866a 100644
--- a/lsp/lib/debug.mli
+++ b/lsp/lib/debug.mli
@@ -24,4 +24,7 @@ class visitor_pp : object
   (** Simplified version od the `scope` method. *)
 end
 
+val pp_expr_text : Tlapm_lib.Expr.T.ctx -> Tlapm_lib.Expr.T.expr Fmt.t
 val pp_expr : Format.formatter -> Tlapm_lib.Expr.T.expr -> unit
+val pp_hyp : Format.formatter -> Tlapm_lib.Expr.T.hyp -> unit
+val pp_cx : Tlapm_lib.Expr.T.hyp Tlapm_lib.Util.Deque.dq Fmt.t
diff --git a/lsp/lib/docs/doc_actual.ml b/lsp/lib/docs/doc_actual.ml
index 382c341b..235a7985 100644
--- a/lsp/lib/docs/doc_actual.ml
+++ b/lsp/lib/docs/doc_actual.ml
@@ -22,7 +22,7 @@ module Parsed = struct
         ~filename:(LspT.DocumentUri.to_path uri)
     with
     | Ok mule ->
-        let ps = Proof_step.of_module mule ps_prev in
+        let ps = Proof_step.of_module mule ?prev:ps_prev in
         { mule = Ok mule; nts = []; ps }
     | Error (loc_opt, msg) ->
         let nts = [ Toolbox.notif_of_loc_msg loc_opt msg ] in
@@ -127,6 +127,7 @@ let is_obl_final (act : t) p_ref obl_id =
   else None
 
 let on_parsed_mule (act : t) f =
-  match (Lazy.force act.parsed).mule with
-  | Ok mule -> ( match f mule with None -> None | Some res -> Some res)
+  let parsed = Lazy.force act.parsed in
+  match parsed.mule with
+  | Ok mule -> f mule (Option.get parsed.ps)
   | Error _ -> None
diff --git a/lsp/lib/docs/doc_actual.mli b/lsp/lib/docs/doc_actual.mli
index eed8cd69..187cc54c 100644
--- a/lsp/lib/docs/doc_actual.mli
+++ b/lsp/lib/docs/doc_actual.mli
@@ -19,4 +19,6 @@ val prover_add_obl : t -> int -> Toolbox.Obligation.t -> t option
 val prover_add_notif : t -> int -> Toolbox.tlapm_notif -> t option
 val prover_terminated : t -> int -> t option
 val is_obl_final : t -> int -> int -> bool option
-val on_parsed_mule : t -> (Tlapm_lib.Module.T.mule -> 'a option) -> 'a option
+
+val on_parsed_mule :
+  t -> (Tlapm_lib.Module.T.mule -> Proof_step.t -> 'a option) -> 'a option
diff --git a/lsp/lib/docs/docs.mli b/lsp/lib/docs/docs.mli
index 0f1182cf..8f146ecf 100644
--- a/lsp/lib/docs/docs.mli
+++ b/lsp/lib/docs/docs.mli
@@ -2,9 +2,41 @@
 
 open Prover
 module LspT := Lsp.Types
+module TL := Tlapm_lib
 
 module Proof_step : sig
   type t
+
+  module El : sig
+    type t =
+      | Module of TL.Module.T.mule
+      | Theorem of {
+          mu : TL.Module.T.modunit;
+          name : TL.Util.hint option;
+          sq : TL.Expr.T.sequent;
+          naxs : int;
+          pf : TL.Proof.T.proof;
+          orig_pf : TL.Proof.T.proof;
+          summ : TL.Module.T.summary;
+        }
+      | Mutate of { mu : TL.Module.T.modunit; usable : TL.Proof.T.usable }
+      | Step of TL.Proof.T.step
+      | Qed of TL.Proof.T.qed_step
+    [@@deriving show]
+  end
+
+  val locate_proof_path : t -> Range.t -> t list
+  val el : t -> El.t * TL.Expr.T.ctx
+  val goal : t -> TL.Proof.T.obligation option
+  val proof : t -> TL.Proof.T.proof option
+  val full_range : t -> Range.t
+  val head_range : t -> Range.t
+  val stepno_seq_under_proof_step : t -> TL.Proof.T.stepno Seq.t
+
+  val stepno_seq_under_stepno :
+    TL.Proof.T.stepno option -> TL.Proof.T.stepno Seq.t
+
+  val sub_step_unnamed : t -> TL.Proof.T.stepno
 end
 
 module Proof_status : sig
@@ -92,9 +124,16 @@ val get_proof_step_details_latest :
     version of the document. *)
 
 val on_parsed_mule :
-  t -> tk -> int -> (Tlapm_lib.Module.T.mule -> 'a option) -> t * 'a option
+  t ->
+  tk ->
+  int ->
+  (Tlapm_lib.Module.T.mule -> Proof_step.t -> 'a option) ->
+  t * 'a option
 (** Apply [f] on a parsed module, if any. *)
 
 val on_parsed_mule_latest :
-  t -> tk -> (int -> Tlapm_lib.Module.T.mule -> 'a option) -> t * 'a option
+  t ->
+  tk ->
+  (int -> Tlapm_lib.Module.T.mule -> Proof_step.t -> 'a option) ->
+  t * 'a option
 (** Apply [f] on a parsed module of the latest version, if any. *)
diff --git a/lsp/lib/docs/obl.ml b/lsp/lib/docs/obl.ml
index 2a41678d..b920f2cb 100644
--- a/lsp/lib/docs/obl.ml
+++ b/lsp/lib/docs/obl.ml
@@ -3,7 +3,7 @@ open Prover
 
 module Role = struct
   type t =
-    | Main  (** Main obligation for a proof step. *)
+    | Main of bool  (** Main obligation for a proof step. *)
     | Aux  (** Auxiliary, created by the prover in the BY clause. *)
     | Unknown  (** Initially all the obligations are of unknown role. *)
     | Unexpected
@@ -11,7 +11,8 @@ module Role = struct
   [@@deriving show]
 
   let as_string = function
-    | Main -> "main"
+    | Main true -> "main"
+    | Main false -> "omitted"
     | Aux -> "aux"
     | Unknown -> "unknown"
     | Unexpected -> "unexpected"
@@ -34,7 +35,6 @@ module ObligationByProverMap = struct
 end
 
 type t = {
-  role : Role.t;
   parsed : Tlapm_lib.Proof.T.obligation option;
       [@printer fun _ fmt -> Printf.ifprintf fmt "...skipped..."]
       (** The obligation as received from the parser. *)
@@ -66,7 +66,6 @@ let of_parsed_obligation (parsed : Tlapm_lib.Proof.T.obligation) =
   let parsed_text_plain = lazy (Some (obl_to_str parsed)) in
   let parsed_text_normalized = lazy (Some (obl_to_normalized_str parsed)) in
   {
-    role = Role.Unknown;
     parsed = Some parsed;
     parsed_text_plain;
     parsed_text_normalized;
@@ -91,8 +90,30 @@ let reset obl p_ref =
     status = Proof_status.Pending;
   }
 
-let with_role role obl = { obl with role }
-let role obl = obl.role
+let parsed obl = obl.parsed
+
+let parsed_main obl =
+  match obl.parsed with
+  | None -> None
+  | Some o -> (
+      match o.kind with
+      | TL.Proof.T.Ob_main | TL.Proof.T.Ob_omitted _ -> Some o
+      | TL.Proof.T.Ob_support | TL.Proof.T.Ob_error _ -> None)
+
+let role obl =
+  match obl.parsed with
+  | None -> Role.Unknown
+  | Some o -> (
+      match o.kind with
+      | Tlapm_lib.Proof.T.Ob_main -> Role.Main true
+      | Tlapm_lib.Proof.T.Ob_support -> Role.Aux
+      | Tlapm_lib.Proof.T.Ob_error _ -> Role.Unexpected
+      | Tlapm_lib.Proof.T.Ob_omitted _ -> Role.Main false)
+
+let is_omitted obl =
+  match role obl with
+  | Role.Main main -> not main
+  | Role.Aux | Role.Unknown | Role.Unexpected -> false
 
 (* Should exist in any case. *)
 let loc obl =
@@ -157,7 +178,6 @@ let with_prover_obligation p_ref (tlapm_obl : Toolbox.Obligation.t)
     match obl with
     | None ->
         {
-          role = Role.Unexpected;
           parsed = None;
           parsed_text_plain = lazy None;
           parsed_text_normalized = lazy None;
@@ -196,7 +216,7 @@ let with_prover_obligation p_ref (tlapm_obl : Toolbox.Obligation.t)
   else if obl.p_ref = p_ref then obl_add obl
   else obl
 
-let with_proof_state_from obl by_fp =
+let with_proof_state_from by_fp obl =
   match obl.latest_prover with
   | None -> (
       match fingerprint obl with
@@ -243,7 +263,7 @@ let as_lsp_diagnostic (obl : t) =
   | false -> None
 
 let as_lsp_tlaps_proof_obligation_state obl =
-  let role = Role.as_string obl.role in
+  let role = role obl |> Role.as_string in
   let range = Range.as_lsp_range (loc obl) in
   let status = Proof_status.to_string obl.status in
   let normalized = text_normalized obl in
diff --git a/lsp/lib/docs/obl.mli b/lsp/lib/docs/obl.mli
index f1ff7799..85400c85 100644
--- a/lsp/lib/docs/obl.mli
+++ b/lsp/lib/docs/obl.mli
@@ -2,18 +2,20 @@ open Util
 open Prover
 
 module Role : sig
-  type t = Main | Aux | Unknown | Unexpected
+  type t = Main of bool | Aux | Unknown | Unexpected
 end
 
 type t
 
 val of_parsed_obligation : Tlapm_lib.Proof.T.obligation -> t
-val with_role : Role.t -> t -> t
 val with_prover_terminated : int -> t -> t
 val with_prover_obligation : int -> Toolbox.Obligation.t -> t option -> t
-val with_proof_state_from : t -> (string -> t option) -> t
+val with_proof_state_from : (string -> t option) -> t -> t
 val with_prover_names : int -> int -> string list -> t -> t
+val parsed : t -> Tlapm_lib.Proof.T.obligation option
+val parsed_main : t -> Tlapm_lib.Proof.T.obligation option
 val role : t -> Role.t
+val is_omitted : t -> bool
 val loc : t -> Range.t
 val fingerprint : t -> string option
 val status : t -> Proof_status.t
diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml
index 4499db0c..6e00774f 100644
--- a/lsp/lib/docs/proof_step.ml
+++ b/lsp/lib/docs/proof_step.ml
@@ -1,125 +1,172 @@
+(* cspell:words mapi modunit summ stepno *)
 open Util
-open Prover
 
-(** We categorize the proof steps just to make the presentation in the UI
-    clearer. *)
-module Kind = struct
-  type t = Module | Struct | Leaf
-
-  let to_string = function
-    | Module -> "module"
-    | Struct -> "struct"
-    | Leaf -> "leaf"
+(** Element of the original AST attached to the user-visible proof step. *)
+module El = struct
+  type t =
+    | Module of TL.Module.T.mule
+    | Theorem of {
+        mu : TL.Module.T.modunit;
+        name : TL.Util.hint option;
+        sq : TL.Expr.T.sequent;
+        naxs : int;
+        pf : TL.Proof.T.proof;
+        orig_pf : TL.Proof.T.proof;
+        summ : TL.Module.T.summary;
+      }
+    | Mutate of { mu : TL.Module.T.modunit; usable : TL.Proof.T.usable }
+    | Step of TL.Proof.T.step
+    | Qed of TL.Proof.T.qed_step
+
+  let pp_short fmt el =
+    match el with
+    | Module m ->
+        Fmt.pf fmt "Module @%a %a" TL.Loc.pp_locus_compact_opt
+          (TL.Util.query_locus m) Fmt.string m.core.name.core
+    | Theorem { name; _ } ->
+        Fmt.pf fmt "Theorem %a"
+          (Fmt.option
+             ~none:(fun fmt () -> Fmt.pf fmt "<unnamed>")
+             TL.Util.pp_print_hint)
+          name
+    | Mutate _ -> Fmt.pf fmt "Mutate"
+    | Step step ->
+        Fmt.pf fmt "Step@%a" TL.Loc.pp_locus_compact_opt
+          (TL.Util.query_locus step)
+    | Qed qed ->
+        Fmt.pf fmt "QED@%a" TL.Loc.pp_locus_compact_opt
+          (TL.Util.query_locus qed)
+
+  let pp = pp_short
+  let show = Fmt.str "%a" pp
 end
 
 type t = {
-  kind : Kind.t;
-      (** Kind/Type of this proof step. We want to show the proof steps
-          differently based in its type. *)
+  el : El.t;
+      (** Kind/Type of this proof step along with the reference to the AST
+          element. *)
+  cx : TL.Expr.T.ctx;  (** Context of the element [el]. *)
   status_parsed : Proof_status.t option;
       (** Status derived at the parse time, if any. This is for the omitted or
           error cases. *)
   status_derived : Proof_status.t;
       (** Derived status. Here we sum-up the states from all the related
           obligations and sub-steps. *)
-  step_loc : Range.t;
-      (** Location of the entire step. It starts with a statement/sequent and
-          ends with the BY keyword (inclusive), not including the listed facts
-          and definitions. In the case of a structured proof, this ends with the
-          BY keyword of the corresponding QED step. *)
-  head_loc : Range.t;
-      (** The location of the proof sequent. It is always contained within the
-          [step_loc]. This is shown as a step in the UI. *)
-  full_loc : Range.t;
+  full_range : Range.t;
       (** [step_loc] plus all the BY facts included. If an obligation is in
-          [full_loc] but not in the [step_loc], we consider it supplementary
+          [full_range] but not in the [step_loc], we consider it supplementary
           (will be shown a bit more hidden). *)
+  head_range : Range.t;
+      (** The location of the proof sequent. It is always contained within the
+          [step_loc]. This is shown as a step in the UI. *)
   obs : Obl.t RangeMap.t;
       (** Obligations associated with this step. Here we include all the
-          obligations fitting into [full_loc], but not covered by any of the
+          obligations fitting into [full_range], but not covered by any of the
           [sub] steps. *)
   sub : t list; (* Sub-steps, if any. *)
 }
 
-(* Derived status is always a minimum of the parsed, the obligations and the sub-steps. *)
+let rec pp_short fmt { el; sub; _ } =
+  Fmt.pf fmt "@[{%a,@ sub=[@[%a@]]}@]" El.pp_short el (Fmt.list pp_short) sub
+
+let pp = pp_short
+let show = Fmt.str "%a" pp
+
+(** We categorize the proof steps just to make the presentation in the UI
+    clearer. *)
+module Kind : sig
+  type ps := t
+  type t = Module | Struct | Leaf | Omitted [@@deriving show]
+
+  val of_proof_step : ps -> t
+  val to_string : t -> string
+end = struct
+  type t = Module | Struct | Leaf | Omitted
+
+  let show = function
+    | Module -> "module"
+    | Struct -> "struct"
+    | Leaf -> "leaf"
+    | Omitted -> "omitted"
+
+  let pp fmt k = Fmt.pf fmt "%s" (show k)
+  let to_string = show
+
+  let of_proof (pf : TL.Proof.T.proof) : t =
+    match pf.core with
+    | TL.Proof.T.Steps (_, _) -> Struct
+    | TL.Proof.T.Omitted _ -> Omitted
+    | TL.Proof.T.Obvious | TL.Proof.T.By _ | TL.Proof.T.Error _ -> Leaf
+
+  let of_proof_step ps =
+    match ps.el with
+    | El.Module _ -> Module
+    | El.Theorem { orig_pf; _ } -> of_proof orig_pf
+    | El.Mutate _ -> Leaf
+    | El.Step st -> (
+        match st.core with
+        | Assert (_, pf) -> of_proof pf
+        | Suffices (_, pf) -> of_proof pf
+        | Pcase (_, pf) -> of_proof pf
+        | Pick (_, _, pf) -> of_proof pf
+        | PickTuply (_, _, pf) -> of_proof pf
+        | TL.Proof.T.Hide _ | TL.Proof.T.Define _ | TL.Proof.T.Use _
+        | TL.Proof.T.Have _ | TL.Proof.T.Take _ | TL.Proof.T.TakeTuply _
+        | TL.Proof.T.Witness _ | TL.Proof.T.Forget _ ->
+            Leaf)
+    | El.Qed qs -> ( match qs.core with TL.Proof.T.Qed pf -> of_proof pf)
+end
+
+(** Derived status is always a minimum of the parsed, the obligations and the
+    sub-steps. *)
 let derived_status parsed obs sub =
   let parsed = Option.value ~default:Proof_status.top parsed in
   let ps_min = Proof_status.min in
   let acc =
-    RangeMap.fold (fun _ obl acc -> ps_min acc (Obl.status obl)) obs parsed
+    RangeMap.fold
+      (fun _ (obl : Obl.t) acc ->
+        (* Do not count omitted obligations. *)
+        if Obl.is_omitted obl then acc else ps_min acc (Obl.status obl))
+      obs parsed
   in
   List.fold_left (fun acc sub -> ps_min acc sub.status_derived) acc sub
 
-(* Takes step parameters and a set of remaining unassigned obligations,
-   constructs the proof step and returns obligations that are left unassigned. *)
-let make ~kind ?status_parsed ~step_loc ?head_loc ~full_loc ~sub obs_map =
-  let intersects_with_full_loc obl_loc _ = Range.intersect obl_loc full_loc in
-  let intersects_with_step_loc obl_loc = Range.intersect obl_loc step_loc in
-  let obs, obs_map = RangeMap.partition intersects_with_full_loc obs_map in
-  let obs =
-    RangeMap.mapi
-      (fun obl_range obl ->
-        match intersects_with_step_loc obl_range with
-        | true -> Obl.with_role Obl.Role.Main obl
-        | false -> Obl.with_role Obl.Role.Aux obl)
-      obs
-  in
-  let head_loc =
+(** Takes step parameters and a set of remaining unassigned obligations,
+    constructs the proof step and returns obligations that are left unassigned.
+*)
+let make ~el ~cx ~status_parsed ~head_range ~full_range =
+  let head_range =
     (* Take the beginning of the first line, if header location is unknown. *)
-    match head_loc with
-    | Some head_loc -> head_loc
-    | None -> Range.(of_points (from step_loc) (from step_loc))
-  in
-  let status_derived = derived_status status_parsed obs sub in
-  let ps =
-    {
-      kind;
-      status_parsed;
-      status_derived;
-      step_loc;
-      head_loc;
-      full_loc;
-      obs;
-      sub;
-    }
+    match head_range with
+    | Some head_range -> Range.(of_points (from full_range) (till head_range))
+    | None -> Range.(of_points (from full_range) (from full_range))
   in
-  (ps, obs_map)
-
-let as_lsp_tlaps_proof_state_marker ps =
-  let status = Proof_status.to_string ps.status_derived in
-  let range = Range.as_lsp_range ps.head_loc in
-  let hover = Proof_status.to_message ps.status_derived in
-  Structs.TlapsProofStepMarker.make ~status ~range ~hover
+  {
+    el;
+    cx;
+    status_parsed;
+    status_derived = Proof_status.Progress;
+    full_range;
+    head_range;
+    obs = RangeMap.empty;
+    sub = [];
+  }
+
+let with_sub ps sub =
+  let status_derived = derived_status ps.status_parsed ps.obs sub in
+  { ps with status_derived; sub }
+
+let with_obs ps obs_map =
+  let in_range obl_loc _ = Range.intersect obl_loc ps.full_range in
+  let obs, obs_map = RangeMap.partition in_range obs_map in
+  let status_derived = derived_status ps.status_parsed obs ps.sub in
+  ({ ps with obs; status_derived }, obs_map)
+
+let with_range ps range =
+  { ps with full_range = Range.join_opt range ps.full_range }
 
-let as_lsp_tlaps_proof_step_details uri ps =
-  let kind = Kind.to_string ps.kind in
-  let status = Proof_status.to_string ps.status_derived in
-  let location =
-    LspT.Location.create ~uri ~range:(Range.as_lsp_range ps.full_loc)
-  in
-  let obligations =
-    List.map
-      (fun (_, o) -> Obl.as_lsp_tlaps_proof_obligation_state o)
-      (RangeMap.to_list ps.obs)
-  in
-  let sub_count =
-    let proved, failed, omitted, missing, pending, progress =
-      List.fold_left
-        (fun (proved, failed, omitted, missing, pending, progress) sub_ps ->
-          match sub_ps.status_derived with
-          | Proved -> (proved + 1, failed, omitted, missing, pending, progress)
-          | Failed -> (proved, failed + 1, omitted, missing, pending, progress)
-          | Omitted -> (proved, failed, omitted + 1, missing, pending, progress)
-          | Missing -> (proved, failed, omitted, missing + 1, pending, progress)
-          | Pending -> (proved, failed, omitted, missing, pending + 1, progress)
-          | Progress -> (proved, failed, omitted, missing, pending, progress + 1))
-        (0, 0, 0, 0, 0, 0) ps.sub
-    in
-    Structs.CountByStepStatus.make ~proved ~failed ~omitted ~missing ~pending
-      ~progress
-  in
-  Structs.TlapsProofStepDetails.make ~kind ~status ~location ~obligations
-    ~sub_count
+(** Iterate over obligations of a particular proof step. *)
+let fold_obs f acc ps = RangeMap.fold (fun _ obl acc -> f acc obl) ps.obs acc
 
 (* Recursively collect all the fingerprinted obligations.
    This is used to transfer proof state from the
@@ -154,260 +201,107 @@ let fold f acc ps =
   in
   match ps with None -> acc | Some ps -> fold_rec acc ps
 
-(** Iterate over obligations of a particular proof step. *)
-let fold_obs f acc ps = RangeMap.fold (fun _ obl acc -> f acc obl) ps.obs acc
-
-module Acc = struct
-  type t = { file : string; obs_map : Obl.t RangeMap.t }
-
-  let some (x, acc) = (Some x, acc)
-  let for_file file acc = file = acc.file
-end
-
-let if_in_file wrapped file fn =
-  match Tlapm_lib.Util.query_locus wrapped with
-  | Some loc when loc.file = file -> fn (Range.of_locus_must loc)
-  | Some _ -> None
-  | None -> None
-
-let if_in_file_acc wrapped acc fn =
-  match Tlapm_lib.Util.query_locus wrapped with
-  | Some loc when Acc.for_file loc.file acc -> fn (Range.of_locus_must loc) acc
-  | Some _ -> (None, acc)
-  | None -> (None, acc)
-
-let rec of_proof step_loc sq_range (proof : Tlapm_lib.Proof.T.proof) acc :
-    t * Acc.t =
-  let open Tlapm_lib in
-  let kind, sub, status_parsed, suppl_loc, acc =
-    match Property.unwrap proof with
-    | Proof.T.Obvious -> (Kind.Leaf, [], None, None, acc)
-    | Proof.T.Omitted omission ->
-        let status_parsed =
-          match omission with
-          | Explicit -> Proof_status.Omitted
-          | Implicit -> Proof_status.Missing
-          | Elsewhere _loc -> Proof_status.Omitted
-        in
-        (Kind.Leaf, [], Some status_parsed, None, acc)
-    | Proof.T.By (usable, _only) ->
-        let wrapped_join_ranges base list =
-          List.fold_left
-            (fun acc d ->
-              match Range.of_wrapped d with
-              | None -> acc
-              | Some r -> Range.join acc r)
-            base list
-        in
-        let suppl_range = step_loc in
-        let suppl_range = wrapped_join_ranges suppl_range usable.defs in
-        let suppl_range = wrapped_join_ranges suppl_range usable.facts in
-        (Kind.Leaf, [], None, Some suppl_range, acc)
-    | Proof.T.Steps (steps, qed_step) ->
-        let acc, sub =
-          List.fold_left_map
-            (fun acc s ->
-              let s, acc = of_step s acc in
-              (acc, s))
-            acc steps
-        in
-        let sub = List.filter_map Fun.id sub in
-        let qed, acc = of_qed_step qed_step acc in
-        let sub = sub @ [ qed ] in
-        let suppl_loc =
-          List.fold_left
-            (fun acc sub_ps -> Range.join acc sub_ps.full_loc)
-            step_loc sub
-        in
-        (Kind.Struct, sub, None, Some suppl_loc, acc)
-    | Proof.T.Error _ -> (Kind.Leaf, [], Some Proof_status.Failed, None, acc)
-  in
-  let head_loc =
-    match sq_range with
-    | Some sq_range -> Some Range.(of_points (from step_loc) (till sq_range))
-    | None -> None
-  in
-  let full_loc =
-    match suppl_loc with
-    | None -> step_loc
-    | Some suppl_loc -> Range.join step_loc suppl_loc
-  in
-  let st, obs_map =
-    make ~kind ?status_parsed ~step_loc ?head_loc ~full_loc ~sub acc.obs_map
-  in
-  (st, { acc with obs_map })
+let el { el; cx; _ } = (el, cx)
 
-and of_implicit_proof_step step_loc suppl_locs (acc : Acc.t) : t * Acc.t =
-  let full_loc = List.fold_left Range.join step_loc suppl_locs in
-  let st, obs_map =
-    make ~kind:Kind.Leaf ~step_loc ~head_loc:step_loc ~full_loc ~sub:[]
-      acc.obs_map
+let goal ({ obs; _ } : t) : TL.Proof.T.obligation option =
+  let found =
+    RangeMap.fold
+      (fun _ o acc ->
+        Option.fold ~none:acc ~some:(fun x -> x :: acc) (Obl.parsed_main o))
+      obs []
   in
-  (st, { acc with obs_map })
-
-(** USE generates aux proof obligations for the facts mentioned, so we create a
-    step for presenting their state. *)
-and of_usable (usable : Tlapm_lib.Proof.T.usable) step_loc (acc : Acc.t) :
-    t option * Acc.t =
-  match usable.facts with
-  | [] -> (None, acc)
-  | first_fact :: _ ->
-      let facts_loc =
-        List.fold_left Range.join
-          (Range.of_wrapped_must first_fact)
-          (List.map Range.of_wrapped_must usable.facts)
-      in
-      let full_loc = Range.join step_loc facts_loc in
-      let st, obs_map =
-        make ~kind:Kind.Leaf ~step_loc ~head_loc:step_loc ~full_loc ~sub:[]
-          acc.obs_map
+  match found with
+  | [] -> None
+  | [ o ] -> Some o
+  | _ :: _ -> (
+      (* Pick the "best" obligation if several of them are found. *)
+      let obl_kind_priority (kind : TL.Proof.T.obligation_kind) : int =
+        match kind with
+        | TL.Proof.T.Ob_main -> 1
+        | TL.Proof.T.Ob_omitted _ -> 2
+        | TL.Proof.T.Ob_support -> 3
+        | TL.Proof.T.Ob_error _ -> 4
       in
-      Acc.some (st, { acc with obs_map })
-
-and of_step (step : Tlapm_lib.Proof.T.step) acc : t option * Acc.t =
-  let open Tlapm_lib in
-  match Property.unwrap step with
-  | Proof.T.Hide _ -> (None, acc)
-  | Proof.T.Define _ -> (None, acc)
-  | Proof.T.Assert (sequent, proof) ->
-      Acc.some
-        (of_proof
-           (Range.of_wrapped_must step)
-           (Range.of_wrapped sequent.active)
-           proof acc)
-  | Proof.T.Suffices (sequent, proof) ->
-      Acc.some
-        (of_proof
-           (Range.of_wrapped_must step)
-           (Range.of_wrapped sequent.active)
-           proof acc)
-  | Proof.T.Pcase (expr, proof) ->
-      Acc.some
-        (of_proof
-           (Range.of_wrapped_must step)
-           (Range.of_wrapped expr) proof acc)
-  | Proof.T.Pick (_bounds, expr, proof) ->
-      Acc.some
-        (of_proof
-           (Range.of_wrapped_must step)
-           (Range.of_wrapped expr) proof acc)
-  | Proof.T.PickTuply (_, expr, proof) ->
-      Acc.some
-        (of_proof
-           (Range.of_wrapped_must step)
-           (Range.of_wrapped expr) proof acc)
-  | Proof.T.Use (usable, _) -> of_usable usable (Range.of_wrapped_must step) acc
-  | Proof.T.Have expr ->
-      let suppl_locs = List.filter_map Range.of_wrapped [ expr ] in
-      Acc.some
-        (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)
-  | Proof.T.Take bounds ->
-      let suppl_locs =
-        List.filter_map (fun (hint, _, _) -> Range.of_wrapped hint) bounds
-      in
-      Acc.some
-        (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)
-  | Proof.T.TakeTuply tuply_bounds ->
-      let suppl_locs =
-        List.concat
-          (List.map
-             (fun (tuply_name, _) ->
-               match tuply_name with
-               | Expr.T.Bound_name hint ->
-                   List.filter_map Range.of_wrapped [ hint ]
-               | Expr.T.Bound_names hints ->
-                   List.filter_map Range.of_wrapped hints)
-             tuply_bounds)
-      in
-      Acc.some
-        (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)
-  | Proof.T.Witness exprs ->
-      let suppl_locs = List.filter_map Range.of_wrapped exprs in
-      Acc.some
-        (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)
-  | Proof.T.Forget _ -> (None, acc)
-
-and of_qed_step (qed_step : Tlapm_lib.Proof.T.qed_step) acc : t * Acc.t =
-  match Tlapm_lib.Property.unwrap qed_step with
-  | Tlapm_lib.Proof.T.Qed proof ->
-      let open Tlapm_lib in
-      let qed_loc = Property.query qed_step Proof.Parser.qed_loc_prop in
-      let qed_range = Range.of_locus_opt qed_loc in
-      of_proof (Range.of_wrapped_must qed_step) qed_range proof acc
-
-(* This is internal function for traversing the modules and module units recursively. *)
-let rec of_submod (mule : Tlapm_lib.Module.T.mule) (acc : Acc.t) :
-    t option * Acc.t =
-  let open Tlapm_lib in
-  if_in_file_acc mule acc @@ fun step_loc acc ->
-  let mule = Property.unwrap mule in
-  let mu_step mu (sub, acc) =
-    let st, acc = of_mod_unit mu acc in
-    let sub = match st with None -> sub | Some st -> st :: sub in
-    (sub, acc)
+      match
+        List.sort
+          (fun o1 o2 ->
+            let open TL.Proof.T in
+            compare (obl_kind_priority o1.kind) (obl_kind_priority o2.kind))
+          found
+      with
+      | [] -> assert false
+      | o :: _ -> Some o)
+
+let proof ({ el; _ } : t) : TL.Proof.T.proof option =
+  match el with
+  | El.Module _ -> None
+  | El.Theorem { orig_pf; _ } -> Some orig_pf
+  | El.Mutate _ -> None
+  | El.Step step -> (
+      match step.core with
+      | TL.Proof.T.Hide _ | TL.Proof.T.Define _
+      | TL.Proof.T.Use (_, _)
+      | TL.Proof.T.Have _ | TL.Proof.T.Take _ | TL.Proof.T.TakeTuply _
+      | TL.Proof.T.Witness _ | TL.Proof.T.Forget _ ->
+          None
+      | TL.Proof.T.Assert (_, pf)
+      | TL.Proof.T.Suffices (_, pf)
+      | TL.Proof.T.Pcase (_, pf)
+      | TL.Proof.T.Pick (_, _, pf)
+      | TL.Proof.T.PickTuply (_, _, pf) ->
+          Some pf)
+  | El.Qed qed -> ( match qed.core with TL.Proof.T.Qed pf -> Some pf)
+
+let full_range { full_range; _ } = full_range
+let head_range { head_range; _ } = head_range
+
+let step_name (ps : t) : TL.Proof.T.stepno option =
+  match ps.el with
+  | El.Module _ | El.Theorem _ | El.Mutate _ -> None
+  | El.Step step -> TL.Property.query step TL.Proof.T.Props.step
+  | El.Qed qed_step -> TL.Property.query qed_step TL.Proof.T.Props.step
+
+(** Level/Depth of a sub-step of a given step. I.e. [x] in
+    {v <x>y v} *)
+let sub_step_no (parent : t) : int =
+  step_name parent |> TL.Proof.T.sub_step_number
+
+let sub_step_label_seq (parent : t) : int Seq.t =
+  let max_num =
+    List.fold_right
+      (fun sub acc ->
+        match step_name sub with
+        | None -> acc
+        | Some sn -> (
+            match sn with
+            | TL.Proof.T.Named (_, label, _) -> (
+                let rec trim_periods s =
+                  if String.ends_with ~suffix:"." s then
+                    String.sub s 0 (String.length s - 1) |> trim_periods
+                  else s
+                in
+                match label |> trim_periods |> int_of_string_opt with
+                | None -> acc
+                | Some x -> max x acc)
+            | TL.Proof.T.Unnamed (_, _) -> acc))
+      parent.sub 0
   in
-  let sub, acc = List.fold_right mu_step mule.body ([], acc) in
-  match sub with
-  | [] -> (None, acc)
-  | _ ->
-      let st, obs_map =
-        make ~kind:Kind.Module ~step_loc ~full_loc:step_loc ~sub acc.obs_map
-      in
-      (Some st, { acc with obs_map })
-
-and of_mod_unit (mod_unit : Tlapm_lib.Module.T.modunit) acc : t option * Acc.t =
-  let open Tlapm_lib in
-  let open Tlapm_lib.Module.T in
-  if_in_file_acc mod_unit acc @@ fun mod_unit_loc acc ->
-  match Property.unwrap mod_unit with
-  | Constants _ -> (None, acc)
-  | Recursives _ -> (None, acc)
-  | Variables _ -> (None, acc)
-  | Definition _ -> (None, acc)
-  | Axiom _ -> (None, acc)
-  | Theorem (_name, sq, _naxs, _prf, prf_orig, _sum) ->
-      Acc.some (of_proof mod_unit_loc (Range.of_wrapped sq.active) prf_orig acc)
-  | Submod sm -> of_submod sm acc
-  | Mutate (`Hide, _) -> (None, acc)
-  | Mutate (`Use _, usable) -> of_usable usable mod_unit_loc acc
-  | Anoninst _ -> (None, acc)
-
-(* This is the entry point for creating proof steps from a module.
-   It will return None, if the module has no provable statements.
-   Otherwise it will return a proof step representing all the module
-   with all the sub-steps for the theorems, and so on. *)
-let of_module (mule : Tlapm_lib.Module.T.mule) prev : t option =
-  match mule.core.stage with
-  | Final fin ->
-      let prev_obs = obl_by_fp prev in
-      let file =
-        match Tlapm_lib.Util.query_locus mule with
-        | None -> failwith "of_module, has no file location"
-        | Some m_locus -> m_locus.file
-      in
-      let mule_obl (o : Tlapm_lib.Proof.T.obligation) =
-        (* Keep only the obligations from the current file. *)
-        if_in_file o.obl file @@ fun o_range ->
-        (* We will use the fingerprints to retain the
-           proof status between the modifications. *)
-        let o =
-          match o.fingerprint with
-          | None -> Tlapm_lib.Backend.Fingerprints.write_fingerprint o
-          | Some _ -> o
-        in
-        let o = Obl.of_parsed_obligation o in
-        let o = Obl.with_proof_state_from o (Hashtbl.find_opt prev_obs) in
-        Some (o_range, o)
-      in
-      let obs = fin.final_obs in
-      let obs = List.filter_map mule_obl (Array.to_list obs) in
-      let obs_map = RangeMap.of_list obs in
-      let acc = Acc.{ file; obs_map } in
-      let step_opt, acc = of_submod mule acc in
-      assert (RangeMap.is_empty acc.obs_map);
-      step_opt
-  | Parsed -> failwith "of_module, parsed"
-  | _ -> failwith "of_module, non final"
+  Seq.ints (max_num + 1)
+
+let stepno_seq_under_proof_step (parent : t) : TL.Proof.T.stepno Seq.t =
+  let sn = sub_step_no parent in
+  sub_step_label_seq parent
+  |> Seq.map (fun sl -> TL.Proof.T.Named (sn, string_of_int sl, false))
+
+let stepno_seq_under_stepno (parent : TL.Proof.T.stepno option) :
+    TL.Proof.T.stepno Seq.t =
+  let sn = TL.Proof.T.sub_step_number parent in
+  Seq.ints 1
+  |> Seq.map (fun sl -> TL.Proof.T.Named (sn, string_of_int sl, false))
+
+let sub_step_unnamed (parent : t) : TL.Proof.T.stepno =
+  let sn = sub_step_no parent in
+  TL.Proof.T.Unnamed (sn, 0)
 
 let with_prover_terminated (ps : t option) p_ref =
   let rec traverse ps =
@@ -445,9 +339,10 @@ let with_provers (ps : t option) p_ref obl_id prover_names =
       let ps, _ = traverse ps in
       Some ps
 
-let with_prover_result (ps : t option) p_ref (pr : Toolbox.Obligation.t) =
-  let rec traverse (ps : t) (pr : Toolbox.Obligation.t) =
-    if Range.intersect ps.full_loc pr.loc then
+let with_prover_result (ps : t option) p_ref (pr : Prover.Toolbox.Obligation.t)
+    =
+  let rec traverse (ps : t) (pr : Prover.Toolbox.Obligation.t) =
+    if Range.intersect ps.full_range pr.loc then
       let apply_to_sub acc sub_ps =
         match acc with
         | true -> (* Already found previously. *) (acc, sub_ps)
@@ -475,10 +370,20 @@ let with_prover_result (ps : t option) p_ref (pr : Toolbox.Obligation.t) =
   | Some ps -> (
       match traverse ps pr with None -> Some ps | Some ps -> Some ps)
 
+let locate_proof_path (ps : t) (r : Range.t) : t list =
+  let rec traverse ps =
+    if Range.lines_intersect ps.full_range r then
+      match List.find_map traverse ps.sub with
+      | None -> Some [ ps ]
+      | Some sub_ps -> Some (ps :: sub_ps)
+    else None
+  in
+  List.rev (Option.value (traverse ps) ~default:[])
+
 (* Find the deepest proof step that intersects line-wise with the specified position. *)
 let locate_proof_step (ps : t option) (position : Range.Position.t) : t option =
   let rec traverse ps =
-    if Range.line_covered ps.full_loc position then
+    if Range.line_covered ps.full_range position then
       match List.find_map traverse ps.sub with
       | None -> Some ps
       | Some sub_ps -> Some sub_ps
@@ -491,9 +396,10 @@ let locate_proof_range (ps : t option) (range : Range.t) : Range.t =
   let ps_till = locate_proof_step ps (Range.till range) in
   match (ps_from, ps_till) with
   | None, None -> Range.of_all
-  | Some ps_from, None -> ps_from.full_loc
-  | None, Some ps_till -> ps_till.full_loc
-  | Some ps_from, Some ps_till -> Range.join ps_from.full_loc ps_till.full_loc
+  | Some ps_from, None -> ps_from.full_range
+  | None, Some ps_till -> ps_till.full_range
+  | Some ps_from, Some ps_till ->
+      Range.join ps_from.full_range ps_till.full_range
 
 let is_obl_final (ps : t option) p_ref obl_id =
   let rec traverse ps =
@@ -506,35 +412,343 @@ let is_obl_final (ps : t option) p_ref obl_id =
   in
   match ps with None -> None | Some ps -> traverse ps
 
+let as_lsp_tlaps_proof_state_marker ps =
+  let status = Proof_status.to_string ps.status_derived in
+  let range = Range.as_lsp_range ps.head_range in
+  let hover = Proof_status.to_message ps.status_derived in
+  Structs.TlapsProofStepMarker.make ~status ~range ~hover
+
+let as_lsp_tlaps_proof_step_details uri ps =
+  let kind = Kind.(of_proof_step ps |> to_string) in
+  let status = Proof_status.to_string ps.status_derived in
+  let location =
+    LspT.Location.create ~uri ~range:(Range.as_lsp_range ps.full_range)
+  in
+  let obligations =
+    List.map
+      (fun (_, o) -> Obl.as_lsp_tlaps_proof_obligation_state o)
+      (RangeMap.to_list ps.obs)
+  in
+  let sub_count =
+    let proved, failed, omitted, missing, pending, progress =
+      List.fold_left
+        (fun (proved, failed, omitted, missing, pending, progress) sub_ps ->
+          match sub_ps.status_derived with
+          | Proved -> (proved + 1, failed, omitted, missing, pending, progress)
+          | Failed -> (proved, failed + 1, omitted, missing, pending, progress)
+          | Omitted -> (proved, failed, omitted + 1, missing, pending, progress)
+          | Missing -> (proved, failed, omitted, missing + 1, pending, progress)
+          | Pending -> (proved, failed, omitted, missing, pending + 1, progress)
+          | Progress -> (proved, failed, omitted, missing, pending, progress + 1))
+        (0, 0, 0, 0, 0, 0) ps.sub
+    in
+    Structs.CountByStepStatus.make ~proved ~failed ~omitted ~missing ~pending
+      ~progress
+  in
+  Structs.TlapsProofStepDetails.make ~kind ~status ~location ~obligations
+    ~sub_count
+
+(** Construct the view of the AST in terms of user-visible proof steps. *)
+module Builder : sig
+  val of_module : TL.Module.T.mule -> t option -> t option
+end = struct
+  let in_file file wrapped =
+    match Tlapm_lib.Util.query_locus wrapped with
+    | Some loc when loc.file = file -> true
+    | Some _ -> false
+    | None -> false
+
+  let if_in_file file cx wrapped fn =
+    match Tlapm_lib.Util.query_locus wrapped with
+    | Some loc when loc.file = file -> fn (Range.of_locus_must loc)
+    | Some _ -> ((cx, wrapped), None)
+    | None -> ((cx, wrapped), None)
+
+  let if_in_file_opt file wrapped fn =
+    match Tlapm_lib.Util.query_locus wrapped with
+    | Some loc when loc.file = file -> fn (Range.of_locus_must loc)
+    | Some _ -> None
+    | None -> None
+
+  let join_range_of_wrapped wrapped acc =
+    List.fold_left
+      (fun acc w ->
+        Range.of_wrapped w |> Option.fold ~none:acc ~some:(Range.join acc))
+      acc wrapped
+
+  let join_range_of_wrapped_opt ?(acc = None) wrapped =
+    List.fold_left
+      (fun acc w ->
+        Range.of_wrapped w
+        |> Option.fold ~none:acc ~some:(fun r -> Some (Range.join_opt acc r)))
+      acc wrapped
+
+  let join_range_of_usable (usable : TL.Proof.T.usable) (acc : Range.t) =
+    acc
+    |> join_range_of_wrapped usable.defs
+    |> join_range_of_wrapped usable.facts
+
+  let join_range_of_usable_opt (usable : TL.Proof.T.usable) =
+    let acc = join_range_of_wrapped_opt usable.defs in
+    join_range_of_wrapped_opt ~acc usable.facts
+
+  (** Derive a status of a step by structure of its proof (as parsed), if
+      possible. *)
+  let parsed_status_of_proof (proof : TL.Proof.T.proof) =
+    match proof.core with
+    | TL.Proof.T.Omitted omission -> (
+        match omission with
+        | TL.Proof.T.Implicit -> Some Proof_status.Missing
+        | TL.Proof.T.Explicit -> Some Proof_status.Omitted
+        | TL.Proof.T.Elsewhere _ -> Some Proof_status.Omitted)
+    | TL.Proof.T.Error _ -> Some Proof_status.Failed
+    | TL.Proof.T.Obvious | TL.Proof.T.By (_, _) | TL.Proof.T.Steps (_, _) ->
+        None
+
+  class step_visitor (file : string) =
+    object (self : 'self)
+      inherit TL.Module.Visit.map as m_super
+      inherit [unit] TL.Proof.Visit.iter as p_super
+      val mutable acc_steps : t list = []
+      val mutable acc_range : Range.t option = None
+      val mutable mu_curr : TL.Module.T.modunit option = None
+      val mutable obs : Obl.t RangeMap.t = RangeMap.empty
+
+      method private take_mu () =
+        let mu = Option.get mu_curr in
+        mu_curr <- None;
+        mu
+
+      method private extend_range r =
+        r
+        |> Option.iter @@ fun r ->
+           let r =
+             match acc_range with
+             | None -> r
+             | Some acc_range -> Range.join acc_range r
+           in
+           acc_range <- Some r
+
+      (* This function mainly here to maintain all the mutable variables in one place. *)
+      method private define_step : 'x. (unit -> 'x * t option) -> 'x =
+        fun f ->
+          let prev_steps = acc_steps in
+          let prev_range = acc_range in
+          acc_steps <- [];
+          acc_range <- None;
+          let res, step = f () in
+          (match step with
+          | None ->
+              assert (acc_steps = []);
+              acc_steps <- prev_steps;
+              acc_range <- prev_range
+          | Some step ->
+              let step = with_sub step (List.rev acc_steps) in
+              let step = with_range step acc_range in
+              let step, obs_remaining = with_obs step obs in
+              acc_steps <- step :: prev_steps;
+              acc_range <- Some (Range.join_opt prev_range step.full_range);
+              obs <- obs_remaining);
+          res
+
+      (* That's the entry point to the visitor. *)
+      method process (mule : TL.Module.T.mule)
+          (prev_obs : (string, Obl.t) Hashtbl.t) : t option =
+        if in_file file mule then (
+          let mule_obl (o : Tlapm_lib.Proof.T.obligation) =
+            (* Keep only the obligations from the current file.
+             We will use the fingerprints to retain the
+             proof status between the modifications.*)
+            if_in_file_opt file o.obl @@ fun o_range ->
+            let o =
+              (match o.fingerprint with
+                | None -> Tlapm_lib.Backend.Fingerprints.write_fingerprint o
+                | Some _ -> o)
+              |> Obl.of_parsed_obligation
+              |> Obl.with_proof_state_from (Hashtbl.find_opt prev_obs)
+            in
+            Some (o_range, o)
+          in
+          obs <-
+            (match mule.core.stage with
+              | TL.Module.T.Special -> []
+              | TL.Module.T.Parsed -> []
+              | TL.Module.T.Flat -> []
+              | TL.Module.T.Final final -> Array.to_list final.final_obs)
+            |> List.filter_map mule_obl |> RangeMap.of_list;
+          ignore (self#tla_module_root mule);
+          assert (RangeMap.is_empty obs);
+          match acc_steps with
+          | [] -> None
+          | [ step ] -> Some step
+          | _ -> assert false)
+        else None
+
+      (* This can be the main module, or any sub-module. *)
+      method! tla_module cx mule =
+        self#define_step @@ fun () ->
+        let cx, mule = m_super#tla_module cx mule in
+        if_in_file file cx mule @@ fun mule_loc ->
+        let step =
+          make ~el:(Module mule) ~status_parsed:None ~cx ~head_range:None
+            ~full_range:mule_loc
+        in
+        ((cx, mule), Some step)
+
+      (* Submodules are not traversed in m_super, thus we traverse them here. *)
+      method! submod cx mule =
+        let cx, mule = self#tla_module cx mule in
+        m_super#submod cx mule
+
+      (* We don't have the range at the theorem, so we try to track it by inspecting module units. *)
+      method! module_unit cx mu =
+        mu_curr <- Some mu;
+        m_super#module_unit cx mu
+
+      (* Leaf at the `Module.Visit.map as m_super`.
+       We will look at `orig_pf`, it is closer to the initial source code. *)
+      method! theorem cx name sq naxs pf orig_pf summ =
+        self#define_step @@ fun () ->
+        let mu = self#take_mu () in
+        let step =
+          if in_file file mu then (
+            Range.of_wrapped mu
+            |> Option.map @@ fun mu_loc ->
+               self#proof ((), cx) orig_pf;
+               let el = El.Theorem { mu; name; sq; naxs; pf; orig_pf; summ } in
+               let full_range = mu_loc in
+               let head_range = Range.(of_wrapped sq.active) in
+               let status_parsed = parsed_status_of_proof orig_pf in
+               make ~el ~cx ~status_parsed ~head_range ~full_range)
+          else None
+        in
+        (m_super#theorem cx name sq naxs pf orig_pf summ, step)
+
+      method! mutate cx change usable =
+        self#define_step @@ fun () ->
+        let mu = self#take_mu () in
+        let use =
+          (* Visible proof steps are only needed for USE with some facts listed. *)
+          match change with
+          | `Use _ -> usable.facts != []
+          | `Hide -> false
+        in
+        let step =
+          if use && in_file file mu then
+            Range.of_wrapped mu
+            |> Option.map @@ fun mu_loc ->
+               let el = El.Mutate { mu; usable } in
+               let full_range = join_range_of_usable usable mu_loc in
+               let head_range = Some full_range in
+               make ~el ~cx ~status_parsed:None ~head_range ~full_range
+          else None
+        in
+        (m_super#mutate cx change usable, step)
+
+      (* Ordinary, non-QED step of a structural proof. *)
+      method! step cx st =
+        self#define_step @@ fun () ->
+        let full_range = Range.of_wrapped_must st in
+        let status_parsed =
+          match TL.Property.unwrap st with
+          | TL.Proof.T.Hide _ | TL.Proof.T.Forget _ | TL.Proof.T.Define _
+          | TL.Proof.T.Have _ | TL.Proof.T.Use _ | TL.Proof.T.Take _
+          | TL.Proof.T.TakeTuply _ | TL.Proof.T.Witness _ ->
+              None
+          | TL.Proof.T.Assert (_, proof)
+          | TL.Proof.T.Suffices (_, proof)
+          | TL.Proof.T.Pcase (_, proof)
+          | TL.Proof.T.Pick (_, _, proof)
+          | TL.Proof.T.PickTuply (_, _, proof) ->
+              parsed_status_of_proof proof
+        in
+        let step = make ~el:(Step st) ~cx:(snd cx) ~status_parsed ~full_range in
+        let step =
+          match TL.Property.unwrap st with
+          | TL.Proof.T.Hide _ | TL.Proof.T.Forget _ | TL.Proof.T.Define _ ->
+              None
+          | TL.Proof.T.Assert (sequent, _proof)
+          | TL.Proof.T.Suffices (sequent, _proof) ->
+              Some (step ~head_range:(Range.of_wrapped sequent.active))
+          | TL.Proof.T.Pcase (expr, _)
+          | TL.Proof.T.Pick (_, expr, _)
+          | TL.Proof.T.PickTuply (_, expr, _) ->
+              Some (step ~head_range:(Range.of_wrapped expr))
+          | TL.Proof.T.Have _ | TL.Proof.T.Take _ | TL.Proof.T.TakeTuply _
+          | TL.Proof.T.Use (_, _)
+          | TL.Proof.T.Witness _ ->
+              Some (step ~head_range:(Some full_range))
+        in
+        (p_super#step cx st, step)
+
+      (* The QED step of a structural proof step. *)
+      method! qed cx qed =
+        self#define_step @@ fun () ->
+        p_super#qed cx qed;
+        let full_range = Range.of_wrapped_must qed in
+        let head_range =
+          TL.Property.query qed TL.Proof.Parser.qed_loc_prop
+          |> Range.of_locus_opt
+        in
+        let status_parsed =
+          match qed.core with
+          | TL.Proof.T.Qed proof -> parsed_status_of_proof proof
+        in
+        let step =
+          make ~el:(Qed qed) ~cx:(snd cx) ~status_parsed ~full_range ~head_range
+        in
+        ((), Some step)
+
+      (* Include all the usable facts to the range of the containing step. *)
+      method! usable cx usable =
+        self#extend_range (join_range_of_usable_opt usable);
+        p_super#usable cx usable
+    end
+
+  (** Make a view of a module in terms of the user-visible proof steps. *)
+  let of_module (mule : TL.Module.T.mule) (prev : t option) : t option =
+    let prev_obs = obl_by_fp prev in
+    let file =
+      match TL.Util.query_locus mule with
+      | None -> failwith "of_module, has no file location"
+      | Some m_locus -> m_locus.file
+    in
+    let v = new step_visitor file in
+    v#process mule prev_obs
+end
+
+let of_module ?prev mule = Builder.of_module mule prev
+
+(* ========================================================================== *)
+
 let%test_unit "determine proof steps" =
   let mod_file = "test_obl_expand.tla" in
   let mod_text =
-    String.concat "\n"
-      [
-        "---- MODULE test_obl_expand ----";
-        "EXTENDS FiniteSetTheorems";
-        "THEOREM FALSE";
-        "    <1>1. TRUE OBVIOUS";
-        "    <1>2. TRUE";
-        "    <1>3. TRUE";
-        "    <1>q. QED BY <1>1, <1>2, <1>3";
-        "THEOREM FALSE";
-        "    <1>q. QED";
-        "       <2>1. TRUE";
-        "       <2>q. QED BY <2>1";
-        "  ----- MODULE sub ------";
-        "  VARIABLE X";
-        "  LEMMA X = X";
-        "  =======================";
-        "====";
-      ]
+    {|
+      ---- MODULE test_obl_expand ----
+      EXTENDS FiniteSetTheorems
+      THEOREM FALSE
+          <1>1. TRUE OBVIOUS
+          <1>2. TRUE
+          <1>3. TRUE
+          <1>q. QED BY <1>1, <1>2, <1>3
+      THEOREM FALSE
+          <1>q. QED
+              <2>1. TRUE
+              <2>q. QED BY <2>1
+        ----- MODULE sub ------
+        VARIABLE X
+        LEMMA X = X
+        =======================
+      ====
+    |}
   in
   let mule =
     Result.get_ok
       (Parser.module_of_string ~content:mod_text ~filename:mod_file
          ~loader_paths:[])
   in
-  let ps = of_module mule None in
+  let ps = of_module mule in
   match flatten ps with
   | [
       _m_test_obl_expand;
@@ -552,18 +766,16 @@ let%test_unit "determine proof steps" =
     ] as all -> (
       List.iteri
         (fun i ps ->
-          Format.printf
-            "Step[%d]: |obs|=%d, full_loc=%s, step_loc=%s head_loc=%s\n" i
+          Format.printf "Step[%d]: |obs|=%d, full_range=%s, head_range=%s\n" i
             (RangeMap.cardinal ps.obs)
-            (Range.string_of_range ps.full_loc)
-            (Range.string_of_range ps.step_loc)
-            (Range.string_of_range ps.head_loc))
+            (Range.string_of_range ps.full_range)
+            (Range.string_of_range ps.head_range))
         all;
       assert (RangeMap.cardinal _th2_1q_2q.obs = 2);
       assert (
         RangeMap.cardinal
           (RangeMap.filter
-             (fun _ o -> Obl.role o = Obl.Role.Main)
+             (fun _ o -> Obl.role o = Obl.Role.Main true)
              _th2_1q_2q.obs)
         = 1);
       let _, _th2_1q_2q_obl = RangeMap.choose _th2_1q_2q.obs in
@@ -578,28 +790,27 @@ let%test_unit "determine proof steps" =
 let%test_unit "determine proof steps for USE statements" =
   let mod_file = "test_use.tla" in
   let mod_text =
-    String.concat "\n"
-      [
-        "---- MODULE test_use ----";
-        "op == TRUE";
-        "USE DEF op";
-        "USE TRUE";
-        "USE FALSE";
-        "HIDE TRUE";
-        "THEOREM TRUE";
-        "    <1> USE TRUE";
-        "    <1> USE FALSE";
-        "    <1> HIDE TRUE";
-        "    <1> QED";
-        "====";
-      ]
+    {|
+      ---- MODULE test_use ----
+      op == TRUE
+      USE DEF op
+      USE TRUE
+      USE FALSE
+      HIDE TRUE
+      THEOREM TRUE
+          <1> USE TRUE
+          <1> USE FALSE
+          <1> HIDE TRUE
+          <1> QED
+      ====
+    |}
   in
   let mule =
     Result.get_ok
       (Parser.module_of_string ~content:mod_text ~filename:mod_file
          ~loader_paths:[])
   in
-  let ps = of_module mule None in
+  let ps = of_module mule in
   match flatten ps with
   | [
       _m_test_use;
@@ -612,12 +823,10 @@ let%test_unit "determine proof steps for USE statements" =
     ] as all ->
       List.iteri
         (fun i ps ->
-          Format.printf
-            "Step[%d]: |obs|=%d, full_loc=%s, step_loc=%s head_loc=%s\n" i
+          Format.printf "Step[%d]: |obs|=%d, full_range=%s, head_range=%s\n" i
             (RangeMap.cardinal ps.obs)
-            (Range.string_of_range ps.full_loc)
-            (Range.string_of_range ps.step_loc)
-            (Range.string_of_range ps.head_loc))
+            (Range.string_of_range ps.full_range)
+            (Range.string_of_range ps.head_range))
         all;
       assert (RangeMap.cardinal _use_true.obs = 1);
       assert (RangeMap.cardinal _use_false.obs = 1)
@@ -628,13 +837,11 @@ let%test_unit "determine proof steps for USE statements" =
 let%test_unit "check if parsing works with nested local instances." =
   let mod_file = "test_loc_ins.tla" in
   let mod_text =
-    String.concat "\n"
-      [
-        (* Just to keep the items wrapped by line. *)
-        "---- MODULE test_loc_ins ----";
-        "LOCAL INSTANCE FiniteSets";
-        "====";
-      ]
+    {|
+      ---- MODULE test_loc_ins ----
+      LOCAL INSTANCE FiniteSets
+      ====
+    |}
   in
   let _mule =
     Result.get_ok
diff --git a/lsp/lib/docs/proof_step.mli b/lsp/lib/docs/proof_step.mli
index c67ab5d7..ab086fcd 100644
--- a/lsp/lib/docs/proof_step.mli
+++ b/lsp/lib/docs/proof_step.mli
@@ -3,20 +3,77 @@
     to the tree as they are obtained from the prover. *)
 
 open Util
-open Prover
 
-type t
+module El : sig
+  type t =
+    | Module of TL.Module.T.mule
+    | Theorem of {
+        mu : TL.Module.T.modunit;
+        name : TL.Util.hint option;
+        sq : TL.Expr.T.sequent;
+        naxs : int;
+        pf : TL.Proof.T.proof;
+        orig_pf : TL.Proof.T.proof;
+        summ : TL.Module.T.summary;
+      }
+    | Mutate of { mu : TL.Module.T.modunit; usable : TL.Proof.T.usable }
+    | Step of TL.Proof.T.step
+    | Qed of TL.Proof.T.qed_step
+  [@@deriving show]
+end
+
+type t [@@deriving show]
+
+val of_module : ?prev:t -> Tlapm_lib.Module.T.mule -> t option
+val el : t -> El.t * TL.Expr.T.ctx
+val goal : t -> TL.Proof.T.obligation option
+val proof : t -> TL.Proof.T.proof option
+val full_range : t -> Range.t
+val head_range : t -> Range.t
+
+val step_name : t -> TL.Proof.T.stepno option
+(** Returns a level and a name of the proof step. [None] is returned if that's a
+    module-level element. *)
+
+val sub_step_label_seq : t -> int Seq.t
+(** Returns a sequence of fresh step names to be used for sub-steps of the
+    provided proof step. *)
+
+val stepno_seq_under_proof_step : t -> TL.Proof.T.stepno Seq.t
+(** Returns a sequence of fresh step names to be used as sub-steps. *)
+
+val stepno_seq_under_stepno :
+  TL.Proof.T.stepno option -> TL.Proof.T.stepno Seq.t
+(** Returns a sequence of fresh step names to be used as sub-steps. *)
+
+val sub_step_unnamed : t -> TL.Proof.T.stepno
+(** Produces a "unnamed" step number for a sub-step of a given step. *)
+
+(** {1 Modifiers.} *)
 
-val of_module : Tlapm_lib.Module.T.mule -> t option -> t option
 val with_prover_terminated : t option -> int -> t option
-val with_prover_result : t option -> int -> Toolbox.Obligation.t -> t option
+
+val with_prover_result :
+  t option -> int -> Prover.Toolbox.Obligation.t -> t option
+
 val with_provers : t option -> int -> int -> string list -> t option
+
+(** {1 Queries} *)
+
+val locate_proof_path : t -> Range.t -> t list
+(** Finds the first deepest proof step covered by the specified range. The
+    result contains the deepest proof step, or an empty list, if no matching
+    step was found at all. *)
+
 val locate_proof_step : t option -> Range.Position.t -> t option
 val locate_proof_range : t option -> Range.t -> Range.t
 val is_obl_final : t option -> int -> int -> bool option
 val flatten : t option -> t list
 val fold : ('a -> t -> 'a) -> 'a -> t option -> 'a
 val fold_obs : ('a -> Obl.t -> 'a) -> 'a -> t -> 'a
+
+(** {1 Conversions} *)
+
 val as_lsp_tlaps_proof_state_marker : t -> Structs.TlapsProofStepMarker.t
 
 val as_lsp_tlaps_proof_step_details :
diff --git a/lsp/lib/docs/util.ml b/lsp/lib/docs/util.ml
index 9f027c76..7c3f7196 100644
--- a/lsp/lib/docs/util.ml
+++ b/lsp/lib/docs/util.ml
@@ -12,6 +12,7 @@ module OblRef = struct
 end
 
 module LspT = Lsp.Types
+module TL = Tlapm_lib
 module DocMap = Map.Make (LspT.DocumentUri)
 module OblMap = Map.Make (OblRef)
 module StrMap = Map.Make (String)
@@ -20,4 +21,4 @@ module RangeMap = Map.Make (Range)
 type parser_fun =
   content:string ->
   filename:string ->
-  (Tlapm_lib.Module.T.mule, string option * string) result
+  (TL.Module.T.mule, string option * string) result
diff --git a/lsp/lib/fmt_marker.ml b/lsp/lib/fmt_marker.ml
new file mode 100644
index 00000000..dc9e325b
--- /dev/null
+++ b/lsp/lib/fmt_marker.ml
@@ -0,0 +1,80 @@
+module IntTable = Hashtbl.Make (Int)
+
+type 'a entry = { value : 'a; from : int; till : int option }
+type 'a t = { mutable out_counter : int; captured : 'a entry IntTable.t }
+
+let create () : 'a t = { out_counter = 0; captured = IntTable.create 10 }
+
+let setup (fmt : Format.formatter) (p : Format.stag -> (int * 'a) option) : 'a t
+    =
+  let cap = create () in
+  Format.pp_set_mark_tags fmt true;
+  let old_stag_functions = Format.pp_get_formatter_stag_functions fmt () in
+  Format.pp_set_formatter_stag_functions fmt
+    {
+      old_stag_functions with
+      mark_open_stag =
+        (fun stag ->
+          (match p stag with
+          | Some (i, v) ->
+              IntTable.add cap.captured i
+                { value = v; from = cap.out_counter; till = None }
+          | None -> ());
+          "");
+      mark_close_stag =
+        (fun stag ->
+          (match p stag with
+          | Some (i, _v) ->
+              let loc = IntTable.find cap.captured i in
+              IntTable.replace cap.captured i
+                { loc with till = Some cap.out_counter }
+          | None -> ());
+          "");
+    };
+  let old_out_functions = Format.pp_get_formatter_out_functions fmt () in
+  Format.pp_set_formatter_out_functions fmt
+    {
+      old_out_functions with
+      out_string =
+        (fun str p n ->
+          cap.out_counter <- cap.out_counter + n;
+          old_out_functions.out_string str p n);
+    };
+  cap
+
+let captured cap = IntTable.to_seq cap.captured |> Seq.map snd |> List.of_seq
+
+let%test_module "" =
+  (module struct
+    (** An example, how to use this module. *)
+
+    (** This part is printing-part dependent. We define a marker, a predicate
+        recognizing it and mark the printed text as needed. The printing side
+        don't need to know anything else. *)
+    type Format.stag += Marker of int
+
+    let is_stag_marker stag =
+      match stag with Marker m -> Some (m, m) | _ -> None
+
+    let pp_x fmt s =
+      Format.pp_open_stag fmt (Marker 13);
+      Fmt.string fmt s;
+      Format.pp_close_stag fmt ()
+
+    (* The function that wants to capture the positions will do the following:
+       setup the formatter, do the printing and then get the captured ranges.
+    *)
+    let%test_unit "usage example" =
+      let b = Buffer.create 10 in
+      let fmt = Format.formatter_of_buffer b in
+      (* ---- Setup the semantic tags. ---------------- *)
+      let cap = setup fmt is_stag_marker in
+      (* ---- Actual printing. ------------------------ *)
+      Fmt.pf fmt "Some@[<v>@;%a@]" pp_x "thing";
+      Format.pp_print_flush fmt ();
+      (* ---- Assert the result. ---------------------- *)
+      let captured = captured cap in
+      assert (String.equal "Some\n    thing" (Buffer.contents b));
+      assert ((List.hd captured).from = 9);
+      assert ((List.hd captured).till = Some 14)
+  end)
diff --git a/lsp/lib/fmt_marker.mli b/lsp/lib/fmt_marker.mli
new file mode 100644
index 00000000..dda9cae2
--- /dev/null
+++ b/lsp/lib/fmt_marker.mli
@@ -0,0 +1,5 @@
+type 'a t
+type 'a entry = private { value : 'a; from : int; till : int option }
+
+val setup : Format.formatter -> (Format.stag -> (int * 'a) option) -> 'a t
+val captured : 'a t -> 'a entry list
diff --git a/lsp/lib/range.ml b/lsp/lib/range.ml
index 2e8a3dd8..45e1ad76 100644
--- a/lsp/lib/range.ml
+++ b/lsp/lib/range.ml
@@ -94,12 +94,27 @@ let of_points f t = R (Position.as_pair f, Position.as_pair t)
 let of_ints ~lf ~cf ~lt ~ct = R ((lf, cf), (lt, ct))
 let of_lines fl tl = R ((fl, 1), (tl, 1))
 let of_len (R ((fl, fc), _)) len = R ((fl, fc), (fl, fc + len - 1))
+let make_before (R ((fl, fc), _)) = R ((fl, fc), (fl, fc - 1))
+let make_before_ln (R ((fl, _), _)) = R ((fl, 1), (fl, 0))
+let make_after (R (_, (tl, tc))) = R ((tl, tc + 1), (tl, tc + 1))
+
+(** Make sure the last line is included completely. *)
+let with_end_line (R (f, (tl, tc))) =
+  if tc = 1 then R (f, (tl, tc)) else R (f, (tl + 1, 0))
 
 let join (R (af, at)) (R (bf, bt)) =
   let f = Position.min (Position.of_pair af) (Position.of_pair bf) in
   let t = Position.max (Position.of_pair at) (Position.of_pair bt) in
   of_points f t
 
+let join_opt a b = match a with None -> b | Some a -> join a b
+
+let join_opt2 a b =
+  match (a, b) with
+  | _, None -> a
+  | None, _ -> b
+  | Some a, Some b -> Some (join a b)
+
 let crop_line_prefix (R ((lf, cf), t)) offset = R ((lf, cf + offset), t)
 
 let string_of_range (R ((fl, fc), (tl, tc))) : string =
diff --git a/lsp/lib/range.mli b/lsp/lib/range.mli
index 4244a130..d480a1d2 100644
--- a/lsp/lib/range.mli
+++ b/lsp/lib/range.mli
@@ -4,6 +4,7 @@ module Position : sig
   type t [@@deriving show]
 
   val compare : t -> t -> int
+  val as_pair : t -> int * int
 end
 
 type t [@@deriving show]
@@ -27,7 +28,13 @@ val of_lines : int -> int -> t
 val of_len : t -> int -> t
 val of_unknown : t
 val of_all : t
+val make_before : t -> t
+val make_before_ln : t -> t
+val make_after : t -> t
+val with_end_line : t -> t
 val join : t -> t -> t
+val join_opt : t option -> t -> t
+val join_opt2 : t option -> t option -> t option
 val crop_line_prefix : t -> int -> t
 val string_of_range : t -> string
 val string_of_pos : Position.t -> string
diff --git a/lsp/lib/seq_acc.ml b/lsp/lib/seq_acc.ml
new file mode 100644
index 00000000..c57c4c9f
--- /dev/null
+++ b/lsp/lib/seq_acc.ml
@@ -0,0 +1,11 @@
+type 'a t = { mutable seq : 'a Seq.t; mutable acc : 'a list }
+
+let make seq = { seq; acc = [] }
+
+let take t =
+  let x, seq = Seq.uncons t.seq |> Option.get in
+  t.seq <- seq;
+  t.acc <- x :: t.acc;
+  x
+
+let acc t = List.rev t.acc
diff --git a/lsp/lib/seq_acc.mli b/lsp/lib/seq_acc.mli
new file mode 100644
index 00000000..4f623a6d
--- /dev/null
+++ b/lsp/lib/seq_acc.mli
@@ -0,0 +1,14 @@
+(** Returns elements from a sequence [seq] one by one and also collects all the
+    returned elements in a list [acc]. This value has mutable fields. *)
+
+type 'a t
+
+val make : 'a Seq.t -> 'a t
+(** Create new taker/accumulator from a sequence. The sequence is assumed to be
+    infinite. *)
+
+val take : 'a t -> 'a
+(** Take next element from the sequence. *)
+
+val acc : 'a t -> 'a list
+(** Return all the elements previously returned by [take]. *)
diff --git a/lsp/lib/server/handlers.ml b/lsp/lib/server/handlers.ml
index 7879a371..1f356966 100644
--- a/lsp/lib/server/handlers.ml
+++ b/lsp/lib/server/handlers.ml
@@ -142,7 +142,10 @@ module Make (CB : Callbacks) = struct
              (CodeActionOptions.create ~resolveProvider:false
                 ~workDoneProgress:false
                 ~codeActionKinds:
-                  [ CodeActionKind.Other "tlaplus.tlaps.check-step.ca" ]
+                  [
+                    CodeActionKind.Other "tlaplus.tlaps.check-step.ca";
+                    CodeActionKind.Refactor;
+                  ]
                 ()))
         ~renameProvider:
           (`RenameOptions
@@ -238,7 +241,7 @@ module Make (CB : Callbacks) = struct
     let pos = Range.of_lsp_position params.position in
     CB.with_docs cb_state @@ fun cb_st docs ->
     let open Analysis.Step_rename in
-    let f _vsn mule = find_ranges pos mule in
+    let f _vsn mule _ps = find_ranges pos mule in
     let docs, res = Docs.on_parsed_mule_latest docs uri f in
     let cb_st =
       match res with
@@ -267,7 +270,7 @@ module Make (CB : Callbacks) = struct
     let newText = params.newName in
     CB.with_docs cb_state @@ fun cb_st docs ->
     let open Analysis.Step_rename in
-    let f _vsn mule = find_ranges pos mule in
+    let f _vsn mule _ps = find_ranges pos mule in
     let docs, res = Docs.on_parsed_mule_latest docs uri f in
     let cb_st =
       match res with
@@ -363,7 +366,7 @@ module Make (CB : Callbacks) = struct
     let cb_state, step_renumber_cas =
       CB.with_docs_res cb_state @@ fun cb_st docs ->
       let open Analysis.Step_renumber.StepInfo in
-      let f _vsn mule =
+      let f _vsn mule _ps =
         let ranges =
           Analysis.Step_renumber.find_ranges
             (Range.of_lsp_range user_range)
@@ -397,6 +400,17 @@ module Make (CB : Callbacks) = struct
       (cb_st, docs, Some actions)
     in
 
+    let cb_state, decompose_cas =
+      CB.with_docs_res cb_state @@ fun cb_st docs ->
+      let f _vsn _mule ps =
+        Some
+          (Analysis.Step_decompose.code_actions uri ps
+             (Range.of_lsp_range user_range))
+      in
+      let docs, res = Docs.on_parsed_mule_latest docs uri f in
+      (cb_st, docs, res)
+    in
+
     (* Suggest "check proof step" action. *)
     let cb_state, check_step_cas =
       let cb_state, res = CB.suggest_proof_range cb_state uri user_range in
@@ -432,8 +446,11 @@ module Make (CB : Callbacks) = struct
 
     (* Return the actions. *)
     let acts =
-      List.append check_step_cas
-        (List.flatten (Option.to_list step_renumber_cas))
+      List.fold_left List.append check_step_cas
+        [
+          Option.value step_renumber_cas ~default:[];
+          Option.value decompose_cas ~default:[];
+        ]
     in
     match acts with
     | [] ->
diff --git a/lsp/lib/structs.ml b/lsp/lib/structs.ml
index 58bc121a..3d1e131f 100644
--- a/lsp/lib/structs.ml
+++ b/lsp/lib/structs.ml
@@ -3,7 +3,7 @@ module LspT = Lsp.Types
 let opt_str o = match o with None -> `Null | Some s -> `String s
 
 (** Corresponds to
-    ```
+    {v
     export interface CountByStepStatus {
       proved: number;
       failed: number;
@@ -12,8 +12,7 @@ let opt_str o = match o with None -> `Null | Some s -> `String s
       pending: number;
       progress: number;
     }
-    ```
-*)
+    v} *)
 module CountByStepStatus = struct
   type t = {
     proved : int;
@@ -40,16 +39,15 @@ module CountByStepStatus = struct
 end
 
 (** Corresponds to
-  ```
-  export interface TlapsProofObligationResult {
-    prover: string;
-    meth: string;
-    status: string;
-    reason: string | null;
-    obligation: string | null; // Non-null, if prover failed.
-  }
-  ```
-*)
+    {v
+    export interface TlapsProofObligationResult {
+      prover: string;
+      meth: string;
+      status: string;
+      reason: string | null;
+      obligation: string | null; // Non-null, if prover failed.
+    }
+    v} *)
 module TlapsProofObligationResult = struct
   type t = {
     prover : string;
@@ -74,16 +72,15 @@ module TlapsProofObligationResult = struct
 end
 
 (** Corresponds to
-  ```
-  export interface TlapsProofObligationState {
-    role: string;
-    range: Range;
-    status: status;
-    normalized: string;
-    results: TlapsProofObligationResult[];
-  }
-  ```
-  *)
+    {v
+    export interface TlapsProofObligationState {
+      role: string;
+      range: Range;
+      status: status;
+      normalized: string;
+      results: TlapsProofObligationResult[];
+    }
+    v} *)
 module TlapsProofObligationState = struct
   type t = {
     role : string;
@@ -109,16 +106,15 @@ module TlapsProofObligationState = struct
 end
 
 (** Corresponds to
-  ```
-  export interface TlapsProofStepDetails {
-    kind: string;
-    status: string;
-    location: Location;
-    obligations: TlapsProofObligationState[];
-    sub_count: CountByStepStatus;
-  }
-  ```
-*)
+    {v
+    export interface TlapsProofStepDetails {
+      kind: string;
+      status: string;
+      location: Location;
+      obligations: TlapsProofObligationState[];
+      sub_count: CountByStepStatus;
+    }
+    v} *)
 module TlapsProofStepDetails = struct
   type t = {
     kind : string;
@@ -159,14 +155,13 @@ module TlapsProofStepDetails = struct
 end
 
 (** Corresponds to
-   ```
-   interface ProofStepMarker {
-     status: string;
-     range: vscode.Range;
-     hover: string;
-   }
-   ```
-*)
+    {v
+    interface ProofStepMarker {
+      status: string;
+      range: vscode.Range;
+      hover: string;
+    }
+    v} *)
 module TlapsProofStepMarker : sig
   type t
 
@@ -186,14 +181,12 @@ end = struct
       ]
 end
 
-(** Passed by the client with the InitializeParams.
-    Corresponds to:
-    ```
+(** Passed by the client with the InitializeParams. Corresponds to:
+    {v
     export interface InitRequestInItializationOptions {
       moduleSearchPaths: string[] | null | undefined
     }
-    ```
-*)
+    v} *)
 module InitializationOptions : sig
   type t
 
@@ -220,14 +213,13 @@ end = struct
     | _ -> { module_search_paths = [] }
 end
 
-(** Returned by the server in response to the Initialize request.
-    Corresponds to:
-    ```
+(** Returned by the server in response to the Initialize request. Corresponds
+    to:
+    {v
     export interface InitResponseCapabilitiesExperimental {
       moduleSearchPaths: string[] | null | undefined
     }
-    ```
-*)
+    v} *)
 module ServerCapabilitiesExperimental : sig
   type t
 
diff --git a/lsp/test/Euclid/Euclid.tla b/lsp/test/Euclid/Euclid.tla
new file mode 100644
index 00000000..f1846494
--- /dev/null
+++ b/lsp/test/Euclid/Euclid.tla
@@ -0,0 +1,105 @@
+---- MODULE Euclid ----
+EXTENDS Integers, GCD
+CONSTANTS M, N
+ASSUME MNPosInt ==
+  /\ M \in Nat \ {0}
+  /\ N \in Nat \ {0}
+
+VARIABLES x, y
+vars == <<x, y>>
+
+NextX == x > y /\ x' = x - y /\ UNCHANGED y
+NextY == x < y /\ y' = y - x /\ UNCHANGED x
+Next == NextX \/ NextY
+Init == x = M /\ y = N
+
+Spec == Init /\ [][Next]_vars
+
+--------------------------------------
+
+PartialCorrectness == x = y => x = GCD(M, N)
+
+TypeOK ==
+  /\ x \in Nat \ {0}
+  /\ y \in Nat \ {0}
+
+IInv == GCD(x, y) = GCD(M, N)
+
+--------------------------------------
+
+INSTANCE TLAPS
+
+THEOREM GCD1 == \A m \in Nat \ {0} : GCD(m, m) = m
+  <1> USE MNPosInt
+  <1> TAKE m \in Nat \ {0}
+  <1>0. m \in Nat OBVIOUS
+  <1>1. Divides(m, m) BY DEF Divides
+  <1>2. \A i \in Nat : Divides(i, m) => (i <= m) BY DEF Divides
+  <1> QED BY <1>0, <1>1, <1>2 DEFS GCD, SetMax, DivisorsOf
+
+THEOREM GCD2 == \A m, n \in Nat \ {0} : GCD(m, n) = GCD(n, m)
+  BY DEFS GCD, SetMax, DivisorsOf, Divides
+
+THEOREM GCD3 == \A m, n \in Nat \ {0} : (n > m) => GCD(m, n) = GCD(m, n - m)
+  <1> USE MNPosInt
+  <1> TAKE m, n \in Nat \ {0}
+  <1> HAVE n > m
+  <1>2. \A i \in Nat : Divides(i, m) /\ Divides(i, n) <=> Divides(i, m) /\ Divides(i, n - m)
+    <2> TAKE i \in Nat
+    <2> m \in Nat /\ n \in Nat OBVIOUS
+    <2>1. Divides(i, m) /\ Divides(i, n) => Divides(i, m) /\ Divides(i, n - m)
+      <3> HAVE (\E q \in Nat : m = q * i) /\ (\E q \in Nat : n = q * i)
+      <3> PICK qm \in Nat : m = qm * i OBVIOUS (* TODO: Crash here. Several obligations. One of them is omitted. *)
+      <3> PICK qn \in Nat : n = qn * i OBVIOUS (* TODO: Crash here. Several obligations. One of them is omitted. *)
+      <3>1. \E q \in Nat : m = q * i BY DEF Divides
+      <3>2. \E q \in Nat : n - m = q * i
+        <4> q == qn - qm
+        <4> HIDE DEF q
+        <4>1. q \in Nat BY DEF q
+        <4>2. USE DEF Divides
+        <4> WITNESS q \in Nat
+        <4> QED BY DEFS Divides, q
+      <3> QED BY <3>1, <3>2 DEF Divides
+    <2>2. Divides(i, m) /\ Divides(i, n - m) => Divides(i, m) /\ Divides(i, n)
+      <3>1. HAVE (\E q \in Nat : m = q * i) /\ (\E q \in Nat : n - m = q * i)
+      <3>2. \E q \in Nat : m = q * i BY <3>1 DEF Divides
+      <3>3. \E q \in Nat : n = q * i
+        <4> PICK qm \in Nat : m = qm * i BY <3>1
+        <4> PICK qd \in Nat : n - m = qd * i BY <3>1
+        <4> q == qm + qd
+        <4> HIDE DEF q
+        <4>1. q \in Nat BY DEF q
+        <4>2. USE <3>1 DEF Divides
+        <4> WITNESS q \in Nat
+        <4> QED BY <3>1 DEF q, Divides
+      <3> QED BY <3>2, <3>3 DEF Divides
+    <2> QED BY <2>1, <2>2
+  <1> QED BY <1>2 DEFS GCD, DivisorsOf, SetMax
+
+
+THEOREM SpecTypeOK == Spec => []TypeOK
+  <1> USE MNPosInt
+  <1>1. Init => TypeOK BY DEFS Init, TypeOK
+  <1>2. TypeOK /\ [Next]_vars => TypeOK' BY DEFS TypeOK, Next, vars, NextX, NextY
+  <1>q. QED BY <1>1, <1>2, PTL DEF Spec
+
+THEOREM Spec => []PartialCorrectness
+  <1> USE GCD1, GCD2, GCD3
+  <1>1. Init => IInv
+    <2>1. HAVE Init
+    <2>q. QED BY <2>1, MNPosInt DEFS IInv, Init, TypeOK
+  <1>2. TypeOK /\ IInv /\ [Next]_vars => IInv'
+    <2>1. HAVE TypeOK /\ IInv /\ [Next]_vars
+    <2>2. TypeOK BY <2>1
+    <2>3. IInv BY <2>1
+    <2>4. [Next]_vars BY <2>1
+    <2>5. CASE Next
+      <3>1. CASE NextX BY <2>1, <3>1 DEFS NextX, IInv, TypeOK
+      <3>2. CASE NextY BY <2>1, <3>2 DEFS NextY, IInv, TypeOK
+      <3> QED BY <2>5, <3>1, <3>2 DEF Next
+    <2>6. CASE UNCHANGED vars BY <2>3, <2>6 DEFS IInv, vars, GCD, TypeOK, SetMax, DivisorsOf
+    <2> QED BY <2>4, <2>5, <2>6
+  <1>3. TypeOK /\ IInv => PartialCorrectness BY DEFS IInv, PartialCorrectness, TypeOK
+  <1>q. QED BY <1>1, <1>2, <1>3, SpecTypeOK, PTL DEF Spec
+
+====
diff --git a/lsp/test/Euclid/GCD.tla b/lsp/test/Euclid/GCD.tla
new file mode 100644
index 00000000..09d90b6b
--- /dev/null
+++ b/lsp/test/Euclid/GCD.tla
@@ -0,0 +1,7 @@
+---- MODULE GCD ----
+EXTENDS Naturals
+Divides(p, n) == \E q \in Nat : n = q * p
+DivisorsOf(n) == { p \in Nat : Divides(p, n) }
+SetMax(S) == CHOOSE i \in S : \A j \in S : i >= j
+GCD(m, n) == SetMax(DivisorsOf(m) \cap DivisorsOf(n))
+====
diff --git a/lsp/test/Makefile b/lsp/test/Makefile
new file mode 100644
index 00000000..56caf0aa
--- /dev/null
+++ b/lsp/test/Makefile
@@ -0,0 +1,11 @@
+all: test
+
+build:
+	dune build
+
+test: build
+	dune test
+
+test-verbose: build
+	(cd ../../_build/default/lsp/test; ./tlapm_lsp_test.exe --verbose)
+
diff --git a/lsp/test/dune b/lsp/test/dune
new file mode 100644
index 00000000..4a1c309c
--- /dev/null
+++ b/lsp/test/dune
@@ -0,0 +1,8 @@
+(test
+ (name tlapm_lsp_test)
+ (build_if
+  (>= %{ocaml_version}, "5.0.0"))
+ (libraries tlapm_lsp_lib lsp alcotest ocolor patdiff)
+ (deps ../bin/tlapm_lsp.exe)
+ (preprocess
+  (pps ppx_deriving.show ppx_deriving.eq)))
diff --git a/lsp/test/test_decompose.ml b/lsp/test/test_decompose.ml
new file mode 100644
index 00000000..b4e91cc5
--- /dev/null
+++ b/lsp/test/test_decompose.ml
@@ -0,0 +1,68 @@
+open Test_utils
+
+let test_to_sub_steps () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW S PROVE \A a, b \in S : a
+    PROOF
+      <1>1. QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW S PROVE \A a, b \in S : a
+    PROOF
+      <1>1. QED
+        <2>1. QED OBVIOUS
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ To sub-steps" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_expand_def () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    Some == TRUE
+    THEOREM Test ==
+        ASSUME NEW S PROVE \A a, b \in Some : a
+    PROOF
+      <1>1. QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    Some == TRUE
+    THEOREM Test ==
+        ASSUME NEW S PROVE \A a, b \in Some : a
+    PROOF
+      <1>1. QED BY DEF Some
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:6 "→ Expand Some" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_cases =
+  let open Alcotest in
+  List.concat
+    [
+      [
+        test_case "To sub-steps" `Quick test_to_sub_steps;
+        test_case "Expand DEF" `Quick test_expand_def;
+      ];
+      Test_decompose_goal.test_cases;
+      Test_decompose_assm.test_cases;
+    ]
diff --git a/lsp/test/test_decompose.tla b/lsp/test/test_decompose.tla
new file mode 100644
index 00000000..42aa92f2
--- /dev/null
+++ b/lsp/test/test_decompose.tla
@@ -0,0 +1,264 @@
+---- MODULE test_decompose ----
+
+Some == TRUE
+
+
+\********************** sub-steps.
+
+THEOREM TestToSubSteps ==
+    ASSUME NEW S PROVE \A a, b \in S : a
+  <1>1. QED OBVIOUS
+
+
+\********************** \A
+
+THEOREM TestGoalForAllBounded ==
+    ASSUME NEW S PROVE \A a, b \in S : a
+PROOF
+  <1> TAKE a, b \in S
+  <1> QED
+
+THEOREM TestGoalForAllUnbounded ==
+    ASSUME NEW S PROVE \A a, b : a
+PROOF
+  <1> TAKE a, b
+  <1> QED
+
+(* Test case: The decompose step should derive `TAKE a_1 \in S`, note `a_1`. *)
+THEOREM TestGoalForAllNameClash ==
+  ASSUME NEW P(_), NEW S
+  PROVE \A a \in S : P(a)
+PROOF
+  <1> a == TRUE
+      a_1 == TRUE
+  <1> HIDE DEF a, a_1
+  \* --------------
+  <1> TAKE a_2 \in S
+  <1>q. QED OBVIOUS
+
+
+\********************** \E
+
+(* TODO: PROOF is not counted to the proof step range. *)
+THEOREM TestGoalExists ==
+  ASSUME NEW P(_, _), NEW S
+  PROVE \E a, b \in S : P(a, b)
+PROOF
+  <1> a == "TODO: Replace this with actual witness for a"
+  <1> b == "TODO: Replace this with actual witness for b"
+  <1> HIDE DEFS a, b
+  <1>4. a \in S 
+  <1>5. b \in S 
+  <1> WITNESS a \in S, b \in S
+  <1>3. QED
+
+THEOREM TestGoalExistsUnderDEF ==
+  ASSUME NEW P(_, _), NEW S
+  PROVE \E a, b \in S : P(a, b)
+PROOF
+  <1> DEFINE Tmp == \E a, b \in S : P(a, b)
+  <1> SUFFICES Tmp OBVIOUS
+  <1> HIDE DEF Tmp
+  \* -----------
+  <1> a == "TODO: Replace this with actual witness for a"
+  <1> b == "TODO: Replace this with actual witness for b"
+  <1> HIDE DEFS a, b
+  <1>5. a \in S 
+  <1>6. b \in S 
+  <1>7. USE DEF Tmp
+  <1> WITNESS a \in S, b \in S
+  <1>4. QED BY DEF Tmp
+
+THEOREM TestGoalExistsUnderOP ==
+  ASSUME NEW P(_, _), NEW S
+  PROVE \E a, b \in S : P(a, b)
+PROOF
+  <1> DEFINE D(X) == \E a, b \in X : P(a, b)
+  <1> SUFFICES D(S) OBVIOUS
+  <1> HIDE DEF D
+  \* -----------
+  <1> a == "TODO: Replace this with actual witness for a"
+  <1> b == "TODO: Replace this with actual witness for b"
+  <1> HIDE DEFS a, b
+  <1>5. a \in S 
+  <1>6. b \in S 
+  <1>7. USE DEF D
+  <1> WITNESS a \in S, b \in S
+  <1>4. QED BY DEF D
+
+
+\* Test case: a symbol bound by \E already defined in the context.
+\* Th decomposition has to pick new/fresh name.
+THEOREM TestGoalExistsNameClash ==
+  ASSUME NEW P(_, _), NEW S
+  PROVE \E a, b \in S : P(a, b)
+PROOF
+  <1> a == TRUE
+  <1> a_1 == TRUE
+  <1> HIDE DEF a, a_1
+  \* -----------
+  <1> a_2 == "TODO: Replace this with actual witness for a_2"
+  <1> b == "TODO: Replace this with actual witness for b"
+  <1> HIDE DEFS a_2, b
+  <1>1. a_2 \in S
+  <1>2. b \in S
+  <1> WITNESS a_2 \in S, b \in S
+  <1>3. QED OBVIOUS \* Decompose here.
+
+
+(* Alternative is to use SUFFICES, but we don't go this way,
+   because we have to analyze then what's in the quantified expression. *)
+THEOREM TestGoalExists2 ==
+  ASSUME NEW P(_), NEW S
+  PROVE \E a \in S : P(a)
+PROOF
+  <1> DEFINE a_witness == TRUE
+  <1> HIDE DEF a_witness
+  <1> SUFFICES a_witness \in S /\ P(a_witness) OBVIOUS
+  <1> QED OBVIOUS
+
+
+\********************** =>
+
+THEOREM TestGoalImplies ==
+    ASSUME NEW a PROVE a => a
+PROOF
+  <1>2. HAVE a
+  <1>1. QED BY <1>2
+
+\********************** /\
+
+THEOREM TestGoalConjunction ==
+  ASSUME NEW a, NEW b, NEW c PROVE a /\ b /\ c
+PROOF
+  <1>1. a OBVIOUS
+  <1>2. b OBVIOUS
+  <1>3. c OBVIOUS
+  <1> QED BY <1>1, <1>2, <1>3
+
+THEOREM TestGoalConjunctionList ==
+    \A a, b, c \in Some :
+        /\ a
+        /\ b
+        /\ c
+PROOF
+  <1> TAKE a, b, c \in Some
+  <1>1. a OBVIOUS
+  <1>2. b OBVIOUS
+  <1>3. c OBVIOUS
+  <1> QED BY <1>1, <1>2, <1>3
+
+\********************** \/
+
+THEOREM TestGoalDisjunction ==
+    \A a, b, c \in Some : a \/ b \/ c
+PROOF
+  <1> TAKE a, b, c \in Some
+  <1>1. SUFFICES ASSUME ~a ,
+                        ~c 
+                 PROVE  b
+        OBVIOUS
+  <1> QED BY <1>1
+
+THEOREM TestGoalDisjunctionList ==
+    \A a, b, c, d \in Some :
+      \/ a
+      \/ b
+      \/ c \/ d
+PROOF
+    <1> TAKE a, b, c, d \in Some
+    <1>1. SUFFICES ASSUME ~b ,
+                          ~c ,
+                          ~d 
+                   PROVE  a
+          OBVIOUS
+    <1> QED BY <1>1
+
+\********************** <=>
+
+THEOREM TestGoalEquiv ==
+  \A a, b \in Some : a <=> b
+PROOF
+  <1> TAKE a, b \in Some
+  <1>1. a => b OBVIOUS
+  <1>2. b => a OBVIOUS
+  <1> QED BY <1>1, <1>2
+
+
+
+THEOREM TestGoalEquiv3 (* TODO: QED Fails to be proved. *) ==
+  \A a, b, c \in Some : a <=> b <=> c
+PROOF
+  <1> TAKE a, b, c \in Some
+  <1>1. a => b OBVIOUS
+  <1>2. b => c
+    <2> HAVE b
+    <2> QED OBVIOUS
+  <1>3. c => a OBVIOUS
+  <1> QED BY <1>1, <1>2, <1>3
+
+
+
+\********************** Assm \/
+
+THEOREM TestAssmDisj ==
+    ASSUME NEW a, NEW b, NEW c, a \/ b
+    PROVE c
+PROOF
+    <1>1. CASE a 
+    <1>2. CASE b 
+    <1> QED BY <1>1, <1>2
+
+\********************** Assm =>
+
+THEOREM TestAssmImplies ==
+    ASSUME NEW a, NEW b, NEW c, NEW d, a => b => c => d
+    PROVE d
+PROOF
+    <1> QED OMITTED
+
+THEOREM TestAssmImplies2 ==
+    ASSUME NEW a, NEW b, NEW c, NEW d, ((a => b) => c) => d
+    PROVE d
+PROOF
+    <1> QED OMITTED
+
+
+
+\********************** Assm \E
+
+THEOREM TestAssmExists ==
+    ASSUME NEW S, \E x \in S : TRUE
+    PROVE S # {}
+PROOF
+    <1>1. PICK x \in S : TRUE OBVIOUS
+    <1> QED BY <1>1
+
+
+\********************** Assm \A
+
+THEOREM TestAssmForall ==
+    ASSUME
+      NEW S,
+      NEW P(_),
+      \A x \in S : P(x),
+      NEW a \in S
+    PROVE P(a)
+PROOF
+  <1>1. PICK x \in S : P(x)
+        <2>1. \E x \in S : TRUE OBVIOUS
+        <2>2. QED BY <2>1
+  <1>q. QED BY <1>1
+
+
+\* ------------------------------------- TODO: debug, temp
+
+DebugOp(S) == \A a, b \in S : a
+
+THEOREM DebugTh1 ==
+    ASSUME NEW S, S = S PROVE DebugOp(S)
+PROOF
+  \* <1> TAKE a, b \in S
+  <1> QED \* BY DEF DebugOp
+
+====
diff --git a/lsp/test/test_decompose_assm.ml b/lsp/test/test_decompose_assm.ml
new file mode 100644
index 00000000..15ed241d
--- /dev/null
+++ b/lsp/test/test_decompose_assm.ml
@@ -0,0 +1,167 @@
+open Test_utils
+
+(** {1 Assm: ∧} *)
+
+let test_assm_conj_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a, NEW b, NEW c, a /\ b /\ c PROVE TRUE
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a, NEW b, NEW c, a /\ b /\ c PROVE TRUE
+    PROOF
+      <1>1. a OBVIOUS
+      <1>2. b OBVIOUS
+      <1>3. c OBVIOUS
+      <1> QED BY <1>1, <1>2, <1>3
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Split (∧): a /\\\\ b /\\\\ c" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Assm: ∨} *)
+
+let test_assm_disj_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a, NEW b, NEW c, a \/ b \/ c PROVE TRUE
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a, NEW b, NEW c, a \/ b \/ c PROVE TRUE
+    PROOF
+      <1>1. CASE a BY <1>1
+      <1>2. CASE b BY <1>2
+      <1>3. CASE c BY <1>3
+      <1> QED BY <1>1, <1>2, <1>3
+    ====
+    |}
+  in
+  let actual =
+    lsp_ca ~lsp ~text ~line:5 "⤮ Case split (∨): a \\\\/ b \\\\/ c"
+  in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Assm: ⇒} *)
+
+let test_assm_implies_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a, NEW b, NEW c, a => b => c PROVE c
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a, NEW b, NEW c, a => b => c PROVE c
+    PROOF
+      <1>1. c
+            <2>1. a OBVIOUS
+            <2>2. b OBVIOUS
+            <2>3. QED BY <2>1, <2>2
+      <1> QED BY <1>1
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Use (⇒): a => (b => c)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Assm: ∀} *)
+
+let test_assm_forall_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW S, NEW P(_), \A x \in S : P(x) PROVE \E x \in S : P(x)
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW S, NEW P(_), \A x \in S : P(x) PROVE \E x \in S : P(x)
+    PROOF
+      <1>1. PICK x \in S : P(x)
+            <2>1. \E x \in S : TRUE OBVIOUS
+            <2>2. QED BY <2>1
+      <1> QED BY <1>1
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Use (∀): \\\\A x \\\\in S : P(x)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Assm: ∃} *)
+
+let test_assm_exists_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW S, NEW P(_), \E x \in S : P(x) PROVE \A x \in S : P(x)
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW S, NEW P(_), \E x \in S : P(x) PROVE \A x \in S : P(x)
+    PROOF
+      <1>1. PICK x \in S : P(x) OBVIOUS
+      <1> QED BY <1>1
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Use (∃): \\\\E x \\\\in S : P(x)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_cases =
+  let open Alcotest in
+  [
+    test_case "Assm ∧, basic" `Quick test_assm_conj_basic;
+    test_case "Assm ∨, basic" `Quick test_assm_disj_basic;
+    test_case "Assm ⇒, basic" `Quick test_assm_implies_basic;
+    test_case "Assm ∀, basic" `Quick test_assm_forall_basic;
+    test_case "Assm ∃, basic" `Quick test_assm_exists_basic;
+  ]
diff --git a/lsp/test/test_decompose_goal.ml b/lsp/test/test_decompose_goal.ml
new file mode 100644
index 00000000..207f369e
--- /dev/null
+++ b/lsp/test/test_decompose_goal.ml
@@ -0,0 +1,489 @@
+open Test_utils
+
+(** {1 Goal: ∀} *)
+
+let test_goal_forall_bounded () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW S PROVE \A a, b \in S : a
+    PROOF
+      <1> QED
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW S PROVE \A a, b \in S : a
+    PROOF
+      <1> TAKE a, b \in S
+      <1> QED
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Decompose goal (∀)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_goal_forall_unbounded () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        \A a, b : a
+    PROOF
+      <1> QED
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        \A a, b : a
+    PROOF
+      <1> TAKE a, b
+      <1> QED
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Decompose goal (∀)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_goal_forall_name_clash () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_), NEW S
+      PROVE \A a \in S : P(a)
+    PROOF
+      <1> a == TRUE
+          a_1 == TRUE
+      <1> HIDE DEF a, a_1
+      <1>q. QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_), NEW S
+      PROVE \A a \in S : P(a)
+    PROOF
+      <1> a == TRUE
+          a_1 == TRUE
+      <1> HIDE DEF a, a_1
+      <1> TAKE a_2 \in S
+      <1>q. QED OBVIOUS
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:9 "⤮ Decompose goal (∀)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Goal: ∃} *)
+
+let test_goal_exists_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1>3. QED
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1> a == "TODO: Replace this with actual witness for a"
+      <1> b == "TODO: Replace this with actual witness for b"
+      <1> HIDE DEFS a, b
+      <1>4. a \in S
+      <1>5. b \in S
+      <1> WITNESS a \in S, b \in S
+      <1>3. QED
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:6 "⤮ Decompose goal (∃)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** Here the \E is not immediate, but under a definition which is expanded. *)
+let test_goal_exists_under_def () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1> DEFINE Tmp == \E a, b \in S : P(a, b)
+      <1> SUFFICES Tmp OBVIOUS
+      <1> HIDE DEF Tmp
+      <1>4. QED BY DEF Tmp
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1> DEFINE Tmp == \E a, b \in S : P(a, b)
+      <1> SUFFICES Tmp OBVIOUS
+      <1> HIDE DEF Tmp
+      <1> a == "TODO: Replace this with actual witness for a"
+      <1> b == "TODO: Replace this with actual witness for b"
+      <1> HIDE DEFS a, b
+      <1>5. a \in S
+      <1>6. b \in S
+      <1>7. USE DEF Tmp
+      <1> WITNESS a \in S, b \in S
+      <1>4. QED BY DEF Tmp
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:9 "⤮ Decompose goal (∃)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** Here the \E is not immediate, but under an expanded operator. *)
+let test_goal_exists_under_op () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1> DEFINE D(X) == \E a, b \in X : P(a, b)
+      <1> SUFFICES D(S) OBVIOUS
+      <1> HIDE DEF D
+      <1>4. QED BY DEF D
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1> DEFINE D(X) == \E a, b \in X : P(a, b)
+      <1> SUFFICES D(S) OBVIOUS
+      <1> HIDE DEF D
+      <1> a == "TODO: Replace this with actual witness for a"
+      <1> b == "TODO: Replace this with actual witness for b"
+      <1> HIDE DEFS a, b
+      <1>5. a \in S
+      <1>6. b \in S
+      <1>7. USE DEF D
+      <1> WITNESS a \in S, b \in S
+      <1>4. QED BY DEF D
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:9 "⤮ Decompose goal (∃)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_goal_exists_name_clash () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1> a == TRUE
+      <1> a_1 == TRUE
+      <1> HIDE DEF a, a_1
+      <1>q. QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW P(_, _), NEW S
+      PROVE \E a, b \in S : P(a, b)
+    PROOF
+      <1> a == TRUE
+      <1> a_1 == TRUE
+      <1> HIDE DEF a, a_1
+      <1> a_2 == "TODO: Replace this with actual witness for a_2"
+      <1> b == "TODO: Replace this with actual witness for b"
+      <1> HIDE DEFS a_2, b
+      <1>1. a_2 \in S
+      <1>2. b \in S
+      <1> WITNESS a_2 \in S, b \in S
+      <1>q. QED OBVIOUS
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:9 "⤮ Decompose goal (∃)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Goal: ⇒} *)
+
+let test_goal_implies_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a PROVE a => a
+    PROOF
+      <1>1. QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+        ASSUME NEW a PROVE a => a
+    PROOF
+      <1>2. HAVE a
+      <1>1. QED BY <1>2
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Decompose goal (⇒)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Goal: ∧} *)
+
+let test_goal_conj_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE a /\ b /\ c
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE a /\ b /\ c
+    PROOF
+      <1>1. a OBVIOUS
+      <1>2. b OBVIOUS
+      <1>3. c OBVIOUS
+      <1> QED BY <1>1, <1>2, <1>3
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Decompose goal (∧)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_goal_conj_list () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE
+        /\ a
+        /\ b /\ c
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE
+        /\ a
+        /\ b /\ c
+    PROOF
+      <1>1. a OBVIOUS
+      <1>2. b OBVIOUS
+      <1>3. c OBVIOUS
+      <1> QED BY <1>1, <1>2, <1>3
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:7 "⤮ Decompose goal (∧)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Goal: ∨} *)
+
+let test_goal_disj_basic_case2 () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE a \/ b \/ c
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE a \/ b \/ c
+    PROOF
+      <1>1. SUFFICES ASSUME ~a ,
+                            ~c
+                    PROVE  b
+            OBVIOUS
+      <1> QED BY <1>1
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Decompose goal (∨, case 2)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_goal_disj_list_case3 () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE
+        \/ a
+        \/ b \/ c
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE
+        \/ a
+        \/ b \/ c
+    PROOF
+      <1>1. SUFFICES ASSUME ~a ,
+                            ~b
+                    PROVE  c
+            OBVIOUS
+      <1> QED BY <1>1
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:7 "⤮ Decompose goal (∨, case 3)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+(** {1 Goal: ≡} *)
+
+let test_goal_equiv_basic () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b PROVE a <=> b
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b PROVE a <=> b
+    PROOF
+      <1>1. a => b OBVIOUS
+      <1>2. b => a OBVIOUS
+      <1> QED BY <1>1, <1>2
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Decompose goal (≡)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_goal_equiv_circular () =
+  let lsp = lsp_init () in
+  let text =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE a <=> b <=> c
+    PROOF
+      <1> QED OBVIOUS
+    ====
+    |}
+  in
+  let expected =
+    {|
+    ---- MODULE test ----
+    THEOREM Test ==
+      ASSUME NEW a, NEW b, NEW c PROVE a <=> b <=> c
+    PROOF
+      <1>1. a => b OBVIOUS
+      <1>2. b => c OBVIOUS
+      <1>3. c => a OBVIOUS
+      <1> QED BY <1>1, <1>2, <1>3
+    ====
+    |}
+  in
+  let actual = lsp_ca ~lsp ~text ~line:5 "⤮ Decompose goal (≡)" in
+  check_multiline_diff_td ~title:"refactoring output" ~expected ~actual;
+  lsp_stop lsp
+
+let test_cases =
+  let open Alcotest in
+  [
+    test_case "Goal ∀, bounded" `Quick test_goal_forall_bounded;
+    test_case "Goal ∀, unbounded" `Quick test_goal_forall_unbounded;
+    test_case "Goal ∀, name clash" `Quick test_goal_forall_name_clash;
+    test_case "Goal ∃, basic" `Quick test_goal_exists_basic;
+    test_case "Goal ∃, under def" `Quick test_goal_exists_under_def;
+    test_case "Goal ∃, under op" `Quick test_goal_exists_under_op;
+    test_case "Goal ∃, name clash" `Quick test_goal_exists_name_clash;
+    test_case "Goal ⇒, basic" `Quick test_goal_implies_basic;
+    test_case "Goal ∧, basic" `Quick test_goal_conj_basic;
+    test_case "Goal ∧, list" `Quick test_goal_conj_list;
+    test_case "Goal ∨, basic, case 2" `Quick test_goal_disj_basic_case2;
+    test_case "Goal ∨, list, case 3" `Quick test_goal_disj_list_case3;
+    test_case "Goal ≡, basic" `Quick test_goal_equiv_basic;
+    test_case "Goal ≡, circular" `Quick test_goal_equiv_circular;
+  ]
diff --git a/lsp/test/test_decompose_naive_bcast.tla b/lsp/test/test_decompose_naive_bcast.tla
new file mode 100644
index 00000000..2df2edd7
--- /dev/null
+++ b/lsp/test/test_decompose_naive_bcast.tla
@@ -0,0 +1,89 @@
+\* cspell:words BCAST
+---- MODULE test_decompose_naive_bcast ----
+CONSTANT Nodes
+CONSTANT Values
+ASSUME Assm == \E n \in Nodes : TRUE
+
+VARIABLE proc
+VARIABLE msgs
+vars == <<proc, msgs>>
+
+Msgs == UNION {
+    [t: {"INPUT"}, v: Values, dst : Nodes],
+    [t: {"BCAST"}, v: Values, dst : Nodes, src : Nodes]
+}
+
+TypeOK ==
+    /\ proc \in [Nodes -> Values]
+    /\ msgs \in SUBSET Msgs
+
+-------------------------
+\* Actions
+
+SendInput ==
+    \E v \in Values, n \in Nodes:
+        /\ msgs' = msgs \cup {[t |-> "INPUT", v |-> v, dst |-> n]}
+        /\ UNCHANGED proc
+
+RecvInput(n) ==
+    \E m \in msgs :
+        /\ m.t = "INPUT"
+        /\ m.dst = n
+        /\ proc' = [proc EXCEPT ![n] = m.v ]
+        /\ msgs' = msgs \cup [t: {"BCAST"}, v: {m.v}, dst : Nodes \ {n}, src : {n}]
+
+RecvBCast(n) ==
+    \E m \in msgs :
+        /\ m.t = "BCAST"
+        /\ m.dst = n
+        /\ proc' = [proc EXCEPT ![n] = m.v ]
+        /\ UNCHANGED msgs
+
+-------------------------
+\* Spec
+
+Init ==
+    /\ \E v \in Values : proc \in [Nodes -> {v}]
+    /\ msgs = {}
+Next ==
+    \/ SendInput
+    \/ \E n \in Nodes :
+        \/ RecvInput(n)
+        \/ RecvBCast(n)
+
+Spec == Init /\ [][Next]_vars
+
+-------------------------
+\* Properties
+
+INSTANCE TLAPS
+
+\* A minimal(ish) version.
+THEOREM Spec => []TypeOK
+    <1> USE DEF TypeOK, Msgs, vars
+    <1>1. Init => TypeOK BY DEFS Init
+    <1>2. TypeOK /\ [Next]_vars => TypeOK'
+      <2> QED BY DEFS Next, RecvBCast, RecvInput, SendInput
+    <1>q. QED BY <1>1, <1>2, PTL DEF Spec
+
+\* The same, just more decomposed.
+THEOREM Spec => []TypeOK
+    <1>1. Init => TypeOK BY DEFS Init, TypeOK, Msgs
+    <1>2. TypeOK /\ [Next]_vars => TypeOK'
+      <2>1. HAVE TypeOK /\ [Next]_vars
+      <2>2. TypeOK BY <2>1
+      <2>3. [Next]_vars BY <2>1
+      <2>4. CASE SendInput BY <2>2, <2>3, <2>4 DEFS Next, SendInput, TypeOK, Msgs
+      <2>5. CASE \E n \in Nodes : \/ RecvInput(n)
+                                  \/ RecvBCast(n)
+        <3>1. PICK n \in Nodes : \/ RecvInput(n)
+                                 \/ RecvBCast(n)
+              BY <2>2, <2>3, <2>5 DEF Next
+        <3>2. CASE RecvInput(n) BY <3>2, <2>2 DEFS Next, RecvInput, TypeOK, Msgs
+        <3>3. CASE RecvBCast(n) BY <3>3, <2>2 DEFS Next, RecvBCast, TypeOK, Msgs
+        <3> QED BY <3>1, <3>2, <3>3 DEF Next
+      <2>6. CASE UNCHANGED vars BY <2>6, <2>2 DEFS vars, TypeOK, Msgs
+      <2> QED BY <2>2, <2>3, <2>4, <2>5, <2>6 DEF Next
+    <1>q. QED BY <1>1, <1>2, PTL DEF Spec
+
+====
diff --git a/lsp/test/test_lsp_client.ml b/lsp/test/test_lsp_client.ml
new file mode 100644
index 00000000..2ad84e53
--- /dev/null
+++ b/lsp/test/test_lsp_client.ml
@@ -0,0 +1,134 @@
+type t = {
+  pid : int;
+  stdin : out_channel;
+  stdout : in_channel;
+  stderr : in_channel;
+  mutable id_seq : Jsonrpc.Id.t Seq.t;
+}
+
+module LspIoState = struct
+  type 'a t = ('a, exn) result
+
+  let return x = Ok x
+  let raise exn = Error exn
+
+  module O = struct
+    let ( let+ ) st f = Result.map f st
+    let ( let* ) st f = Result.bind st f
+  end
+end
+
+module LspIoChan = struct
+  type input = in_channel
+  type output = out_channel
+
+  let read_line (i : input) : string option LspIoState.t =
+    let line = input_line i in
+    Ok (Some line)
+
+  let read_exactly (i : input) (n : int) : string option LspIoState.t =
+    let data = In_channel.really_input_string i n in
+    Ok data
+
+  let write (o : output) (lines : string list) : unit LspIoState.t =
+    lines |> List.iter (Out_channel.output_string o);
+    Out_channel.flush o;
+    Ok ()
+end
+
+module LspIo = Lsp.Io.Make (LspIoState) (LspIoChan)
+
+let run cmd : t =
+  let stdin_r, stdin_w = Unix.pipe () in
+  let stdout_r, stdout_w = Unix.pipe () in
+  let stderr_r, stderr_w = Unix.pipe () in
+  let pid =
+    Unix.create_process cmd
+      [| cmd; "--stdio"; "--log-io"; "--log-to=test_lsp_client.log" |]
+      stdin_r stdout_w stderr_w
+  in
+  {
+    pid;
+    stdin = Unix.out_channel_of_descr stdin_w;
+    stdout = Unix.in_channel_of_descr stdout_r;
+    stderr = Unix.in_channel_of_descr stderr_r;
+    id_seq = Seq.ints 1 |> Seq.map (fun i -> `Int i);
+  }
+
+let close (t : t) : unit =
+  In_channel.close t.stdout;
+  Out_channel.close t.stdin;
+  In_channel.close t.stdout;
+  In_channel.close t.stderr;
+  Unix.kill t.pid Sys.sigint;
+  ()
+
+let next_id (t : t) : Jsonrpc.Id.t =
+  let id, seq = Seq.uncons t.id_seq |> Option.get in
+  t.id_seq <- seq;
+  id
+
+let pp_packet fmt (p : Jsonrpc.Packet.t) : unit =
+  Yojson.Safe.pretty_print fmt (Jsonrpc.Packet.yojson_of_t p)
+
+let send_packet (t : t) (p : Jsonrpc.Packet.t) : unit =
+  match LspIo.write t.stdin p with Ok () -> () | Error exn -> raise exn
+
+let send_request (t : t) req =
+  let id = next_id t in
+  let json_request = Lsp.Client_request.to_jsonrpc_request ~id req in
+  let json_packet = Jsonrpc.Packet.Request json_request in
+  send_packet t json_packet;
+  id
+
+let send_notification t n =
+  let json_notif = Lsp.Client_notification.to_jsonrpc n in
+  let json_packet = Jsonrpc.Packet.Notification json_notif in
+  send_packet t json_packet
+
+let recv_packet (t : t) : Jsonrpc.Packet.t option =
+  match LspIo.read t.stdout with Ok data -> data | Error exn -> raise exn
+
+let rec recv_response ?(log : bool = true) t id =
+  match recv_packet t with
+  | None -> assert false
+  | Some p -> (
+      if log then Fmt.epr "Packet received: %a@." pp_packet p;
+      match p with
+      | Response { id = resp_id; result } when resp_id = id ->
+          result |> Result.get_ok
+      | _ -> recv_response t id)
+
+let call t r = send_request t r |> recv_response t
+
+let call_init t =
+  Lsp.Client_request.Initialize
+    Lsp.Types.InitializeParams.
+      {
+        processId = Some 42;
+        capabilities =
+          Lsp.Types.ClientCapabilities.
+            {
+              workspace = None;
+              experimental = None;
+              window = None;
+              textDocument = None;
+              notebookDocument = None;
+              general = None;
+            };
+        clientInfo = None;
+        locale = None;
+        rootPath = None;
+        rootUri = None;
+        initializationOptions = None;
+        trace = None;
+        workDoneToken = None;
+        workspaceFolders = None;
+      }
+  |> call t |> Lsp.Types.InitializeResult.t_of_yojson
+
+let print_stderr (t : t) : unit =
+  (* Fmt.epr "%s@." (In_channel.input_all t.stderr) *)
+  match In_channel.input_line t.stderr with
+  | None -> ()
+  | Some line -> Fmt.epr "%s@." line
diff --git a/lsp/test/test_lsp_client.mli b/lsp/test/test_lsp_client.mli
new file mode 100644
index 00000000..f120df9a
--- /dev/null
+++ b/lsp/test/test_lsp_client.mli
@@ -0,0 +1,13 @@
+type t
+
+val run : string -> t
+val close : t -> unit
+val send_packet : t -> Jsonrpc.Packet.t -> unit
+val send_request : t -> 'a Lsp.Client_request.t -> Jsonrpc.Id.t
+val send_notification : t -> Lsp.Client_notification.t -> unit
+val recv_packet : t -> Jsonrpc.Packet.t option
+val recv_response : ?log:bool -> t -> Jsonrpc.Id.t -> Jsonrpc.Json.t
+val call : t -> 'a Lsp.Client_request.t -> Jsonrpc.Json.t
+val call_init : t -> Lsp.Types.InitializeResult.t
+val print_stderr : t -> unit
+val next_id : t -> Jsonrpc.Id.t
diff --git a/lsp/test/test_utils.ml b/lsp/test/test_utils.ml
new file mode 100644
index 00000000..cb5de190
--- /dev/null
+++ b/lsp/test/test_utils.ml
@@ -0,0 +1,165 @@
+module MultilineDiff : sig
+  (** For comparing module texts showing multiline diff. *)
+
+  include Alcotest.TESTABLE
+
+  val same : t
+  val diff : string -> string -> t
+end = struct
+  type t = Same | Differs of string
+
+  let same = Same
+
+  let diff a b =
+    let open Patdiff in
+    let prev = Diff_input.{ name = "a"; text = a } in
+    let next = Diff_input.{ name = "b"; text = b } in
+    let diff = Compare_core.diff_strings Configuration.default ~prev ~next in
+    match diff with `Same -> Same | `Different s -> Differs s
+
+  let pp fmt (t : t) =
+    match t with
+    | Same -> Fmt.string fmt "Same"
+    | Differs d -> Fmt.pf fmt "Differs\n%s@." d
+
+  let equal a b =
+    match (a, b) with
+    | Same, Same -> true
+    | Same, Differs _ -> false
+    | Differs _, Same -> false
+    | Differs _, Differs _ -> failwith "cannot compare non empty diffs"
+end
+
+let check_multiline_diff ~title ~expected ~actual =
+  Alcotest.check
+    (module MultilineDiff)
+    title MultilineDiff.same
+    (MultilineDiff.diff expected actual)
+
+let check_multiline_diff_td ~title ~expected ~actual =
+  check_multiline_diff ~title ~expected ~actual:(Lsp.Text_document.text actual)
+
+module CodeActionFound : sig
+  (** Attempt to make test results a bit more understandable in the case of
+      wrong code actions proposed. *)
+
+  include Alcotest.TESTABLE
+
+  val find :
+    string ->
+    [ `CodeAction of Lsp.Types.CodeAction.t | `Command of Lsp.Types.Command.t ]
+    list ->
+    t * t
+
+  val get : t -> Lsp.Types.CodeAction.t
+end = struct
+  type t =
+    | Found of Lsp.Types.CodeAction.t
+    | NotFound of string * string list
+    | Expected of string
+
+  let pp fmt (t : t) =
+    match t with
+    | Found _ -> Fmt.string fmt "Found"
+    | Expected pattern -> Fmt.pf fmt "Expected %s" pattern
+    | NotFound (pattern, titles) ->
+        Fmt.pf fmt "\nNotFound %s\nReceived:\n  %a" pattern
+          (Fmt.list ~sep:Fmt.(const string "\n  ") Fmt.string)
+          titles
+
+  let equal a b =
+    match (a, b) with Found _, _ | _, Found _ -> true | _ -> false
+
+  let get a = match a with Found x -> x | _ -> assert false
+
+  let strings_of_cas cas =
+    cas
+    |> List.map (fun x ->
+        let open Lsp.Types in
+        match x with
+        | `Command ({ title; _ } : Command.t) -> Fmt.str "Command: %s" title
+        | `CodeAction ({ title; _ } : CodeAction.t) ->
+            Fmt.str "CodeAction: %s" title)
+
+  let find pattern cas =
+    let found =
+      cas
+      |> List.find_map (fun x ->
+          let open Lsp.Types in
+          match x with
+          | `Command (_ : Command.t) -> None
+          | `CodeAction (ca : CodeAction.t) ->
+              if Str.string_match (Str.regexp pattern) ca.title 0 then Some ca
+              else None)
+    in
+    let found =
+      match found with
+      | None -> NotFound (pattern, strings_of_cas cas)
+      | Some ca -> Found ca
+    in
+    (found, Expected pattern)
+end
+
+let check_ca_proposed ~expected ~actual =
+  Alcotest.check
+    (module CodeActionFound)
+    "Code Action should be proposed" expected actual
+
+(** {1 Helpers for invoking LSP}*)
+
+let lsp_init () =
+  let lsp = Test_lsp_client.run "../bin/tlapm_lsp.exe" in
+  let init_response = Test_lsp_client.call_init lsp in
+  Alcotest.(
+    check string "serverInfo.name" "tlapm-lsp"
+      (init_response.serverInfo |> Option.get).name);
+  Test_lsp_client.send_notification lsp Lsp.Client_notification.Initialized;
+  lsp
+
+let lsp_stop lsp = Test_lsp_client.close lsp
+
+(** Invoke a Code Action at the specified line. *)
+let lsp_ca ~lsp ?(name = "test") ~text ~line ca_regex =
+  let path = Fmt.str "file:///tmp/%s.tla" name in
+  let uri = Lsp.Uri.of_string path in
+
+  let languageId = "tlaplus" in
+  let did_open_doc_params =
+    Lsp.Types.(
+      DidOpenTextDocumentParams.create
+        ~textDocument:
+          (TextDocumentItem.create ~languageId ~text ~uri ~version:1))
+  in
+  Test_lsp_client.send_notification lsp
+    (Lsp.Client_notification.TextDocumentDidOpen did_open_doc_params);
+
+  let ca_response =
+    let open Lsp.Types in
+    Lsp.Client_request.CodeAction
+      (CodeActionParams.create
+         ~textDocument:(TextDocumentIdentifier.create ~uri)
+         ~range:
+           (Range.create
+              ~start:(Position.create ~line ~character:0)
+              ~end_:(Position.create ~line ~character:0))
+         ~context:(CodeActionContext.create ~diagnostics:[] ())
+         ())
+    |> Test_lsp_client.call lsp |> CodeActionResult.t_of_yojson |> Option.get
+  in
+  let ca_expected =
+    let found, expected = CodeActionFound.find ca_regex ca_response in
+    check_ca_proposed ~expected ~actual:found;
+    CodeActionFound.get found
+  in
+  let (actual : Lsp.Text_document.t) =
+    let text_doc =
+      Lsp.Text_document.make ~position_encoding:`UTF8 did_open_doc_params
+    in
+    Lsp.Text_document.apply_text_document_edits text_doc
+      Lsp.Types.(
+        ca_expected.edit |> Option.to_list
+        |> List.map (fun (e : WorkspaceEdit.t) ->
+            e.changes |> Option.get |> List.map snd |> List.flatten)
+        |> List.flatten)
+  in
+  actual
diff --git a/lsp/test/test_utils.mli b/lsp/test/test_utils.mli
new file mode 100644
index 00000000..7cae607c
--- /dev/null
+++ b/lsp/test/test_utils.mli
@@ -0,0 +1,16 @@
+val check_multiline_diff :
+  title:string -> expected:string -> actual:string -> unit
+
+val check_multiline_diff_td :
+  title:string -> expected:string -> actual:Lsp.Text_document.t -> unit
+
+val lsp_init : unit -> Test_lsp_client.t
+val lsp_stop : Test_lsp_client.t -> unit
+
+val lsp_ca :
+  lsp:Test_lsp_client.t ->
+  ?name:string ->
+  text:string ->
+  line:int ->
+  string ->
+  Lsp.Text_document.t
diff --git a/lsp/test/tlapm_lsp_test.ml b/lsp/test/tlapm_lsp_test.ml
new file mode 100644
index 00000000..34007df4
--- /dev/null
+++ b/lsp/test/tlapm_lsp_test.ml
@@ -0,0 +1,11 @@
+open Test_utils
+
+let test_lsp_init () = lsp_init () |> lsp_stop
+
+let () =
+  let open Alcotest in
+  run "tlapm_lsp"
+    [
+      ("meta", [ test_case "Init" `Quick test_lsp_init ]);
+      ("decompose", Test_decompose.test_cases);
+    ]
diff --git a/src/backend/prep.ml b/src/backend/prep.ml
index 00d94257..6945c30d 100644
--- a/src/backend/prep.ml
+++ b/src/backend/prep.ml
@@ -585,7 +585,7 @@ let trying_to_prove_true = function
 (* FIXME printing should probably be done in save_result *)
 let trivial ob =
   match ob.kind with
-  | Ob_main -> raise Nontrivial
+  | Ob_main | Ob_omitted _ -> raise Nontrivial
   | Ob_support ->
       let sq = ob.obl.core in
       let cx = if (trying_to_prove_true sq.active.core)
diff --git a/src/backend/toolbox.ml b/src/backend/toolbox.ml
index 2168a8a2..80bc7285 100644
--- a/src/backend/toolbox.ml
+++ b/src/backend/toolbox.ml
@@ -27,6 +27,7 @@ let toolbox_print ob ?(temp=false) status prover meth timeout already print_ob
       match ob.kind with
       | Ob_error msg when print_ob ->
           Some (warnings ^ msg)
+      | Ob_omitted _ -> None
       | _ when print_ob ->
           let buf = Buffer.create 100 in
           let ff = Format.formatter_of_buffer buf in
@@ -97,8 +98,6 @@ let print_new_res ob st warns time_used =
 
 (**** duplicates prep.ml *****)
 let expand_defs ?(what = fun _ -> true) ob =
-  let prefix = ref [] in
-  let emit mu = prefix := mu :: (!prefix) in
   let rec visit sq =
     match Deque.front sq.context with
     | None -> sq
@@ -107,7 +106,6 @@ let expand_defs ?(what = fun _ -> true) ob =
           | Defn ({core = Operator (_, e)}, wd, Visible, _) when what wd ->
               visit (app_sequent (scons e (shift 0)) { sq with context = hs })
           | _ ->
-              emit h ;
               let sq = visit { sq with context = hs } in
                 { sq with context = Deque.cons h sq.context }
       end
diff --git a/src/ctx.ml b/src/ctx.ml
index 454ac393..739d7d57 100644
--- a/src/ctx.ml
+++ b/src/ctx.ml
@@ -28,13 +28,15 @@ type 'a ctx = {
   linrep : (ident * 'a option) list ;
   idents : ident M.t ;
   defns  : ('a option * int) M.t ;
-  length : int
+  length : int ;
+  try_print_src : bool
 }
 
 let dot = { linrep = [] ;
             idents = M.empty ;
             defns  = M.empty ;
-            length = 0 }
+            length = 0 ;
+            try_print_src = false}
 
 let length cx = cx.length
 
@@ -75,10 +77,11 @@ let maybe_adj cx v a =
         { id with salt = id.salt + 1 }
   in
   let id = find_id id in
-    { linrep = (id, a) :: cx.linrep ;
+    { cx with
+      linrep = (id, a) :: cx.linrep ;
       idents = M.add v id cx.idents ;
       defns  = M.add (string_of_ident id) (a, cx.length) cx.defns ;
-      length = cx.length + 1 }
+      length = cx.length + 1}
 
 let adj cx v a = maybe_adj cx v (Some a)
 
@@ -124,6 +127,9 @@ let pp_print_ident ff id =
   Format.fprintf ff "%s.%d" id.rep id.salt
   (* pp_print_string ff (string_of_ident id) *)
 
+let with_try_print_src cx = { cx with try_print_src = true }
+let try_print_src {try_print_src; _} = try_print_src
+
 let pp_print_ctx fmt ff cx =
   let rec pp ff = function
     | [] -> ()
diff --git a/src/ctx.mli b/src/ctx.mli
index 3dc1e93f..7a1ee47e 100644
--- a/src/ctx.mli
+++ b/src/ctx.mli
@@ -3,6 +3,8 @@
 Copyright (C) 2008-2010  INRIA and Microsoft Corporation
 *)
 type 'a ctx
+
+(** Stands for an identifier. Used to resolve name clashes by appending a number suffix. *)
 type ident = { rep : string ; salt : int }
 
 val length: 'a ctx -> int
@@ -36,6 +38,10 @@ val depth: 'a ctx -> string -> int option
 
 val to_list: 'a ctx -> 'a list
 
+(** To print the opaque elements without ? appended to them. *)
+val with_try_print_src : 'a ctx -> 'a ctx
+val try_print_src : 'a ctx -> bool
+
 val string_of_ident: ident -> string
 val pp_print_ident:
     Format.formatter -> ident -> unit
diff --git a/src/expr.mli b/src/expr.mli
index c96e1aec..9d648fcc 100644
--- a/src/expr.mli
+++ b/src/expr.mli
@@ -16,7 +16,7 @@ module T: sig
 
   type quantifier = Forall | Exists
 
-  type modal_op = Box | Dia
+  type modal_op = Box | Dia [@@deriving show]
 
   type fairness_op  = Weak | Strong
 
diff --git a/src/expr/e_fmt.ml b/src/expr/e_fmt.ml
index f86704be..328dd1e5 100644
--- a/src/expr/e_fmt.ml
+++ b/src/expr/e_fmt.ml
@@ -18,7 +18,7 @@ open Property
 open E_t
 open Format
 open Fmtutil
-open Tla_parser
+module Fu = Tla_parser.Fu
 
 
 type ctx = hyp Deque.dq * int Ctx.ctx
@@ -463,7 +463,9 @@ and fmt_apply (hx, vx as cx) op args = match op.core, args with
             let top = Optable.lookup s in
             (* coalescing leads to this case, prepending "?" to the newly
             introduced identifiers. *)
-            { top with Optable.name = "?" ^ top.Optable.name }
+            if Ctx.try_print_src (snd cx)
+              then top
+              else { top with Optable.name = "?" ^ top.Optable.name }
         | Internal b ->
             Optable.standard_form b
         | _ ->
diff --git a/src/expr/e_t.ml b/src/expr/e_t.ml
index 433c9c9d..d407f213 100644
--- a/src/expr/e_t.ml
+++ b/src/expr/e_t.ml
@@ -23,7 +23,7 @@ type bullet  = And | Or | Refs
 
 type quantifier = Forall | Exists
 
-type modal_op = Box | Dia
+type modal_op = Box | Dia [@@deriving show]
 
 type fairness_op  = Weak | Strong
 
diff --git a/src/expr/e_t.mli b/src/expr/e_t.mli
index e3d31791..1f7390a4 100644
--- a/src/expr/e_t.mli
+++ b/src/expr/e_t.mli
@@ -20,7 +20,7 @@ case as similar to [And].
 *)
 type bullet = And | Or | Refs
 type quantifier = Forall | Exists
-type modal_op = Box | Dia
+type modal_op = Box | Dia [@@deriving show]
 type fairness_op  = Weak | Strong
 
 (** Type representing arguments to
diff --git a/src/proof.mli b/src/proof.mli
index 94fd05d5..fad71bd2 100644
--- a/src/proof.mli
+++ b/src/proof.mli
@@ -38,7 +38,11 @@ module T : sig
   and use_def =
     | Dvar of string
     | Dx   of int
-  type obligation_kind = Ob_main | Ob_support | Ob_error of string
+  type obligation_kind =
+    | Ob_main
+    | Ob_support
+    | Ob_error of string
+    | Ob_omitted of omission
   type obligation = {
     id  : int option;
     obl : sequent wrapped;
@@ -62,6 +66,7 @@ module T : sig
   val string_of_stepno: ?anonid:bool -> stepno -> string
   val get_qed_proof: qed_step_ Property.wrapped -> proof
   val step_number: stepno -> int
+  val sub_step_number : stepno option -> int
 end
 
 module Fmt : sig
@@ -101,6 +106,7 @@ module Visit : sig
     method proof  : 's scx -> proof -> unit
     method steps  : 's scx -> step list -> 's scx
     method step   : 's scx -> step -> 's scx
+    method qed    : 's scx -> qed_step -> unit
     method usable : 's scx -> usable -> unit
   end
 end
diff --git a/src/proof/p_fmt.ml b/src/proof/p_fmt.ml
index 210f5f0c..b1693223 100644
--- a/src/proof/p_fmt.ml
+++ b/src/proof/p_fmt.ml
@@ -106,6 +106,13 @@ let rec pp_print_proof cx ff prf =
               (prmeth prf)
         | Obvious ->
             fprintf ff "%sOBVIOUS%t" supp (prmeth prf)
+        | Omitted h when Ctx.try_print_src (snd cx) ->
+            fprintf ff "%s%s" supp begin
+              match h with
+                | Explicit -> "OMITTED"
+                | Implicit -> ""
+                | Elsewhere loc -> Printf.sprintf "OMITTED (* see %s *)" (Loc.string_of_locus ~cap:false loc)
+            end
         | Omitted h ->
             fprintf ff "%sOMITTED%s" supp begin
               match h with
@@ -125,8 +132,8 @@ let rec pp_print_proof cx ff prf =
                    cx)
                 cx ff inits
             in
-            fprintf ff "@[<hv2>%s%s QED%a@]"
-              (step_name prf) (step_dot prf)
+            fprintf ff "@[<hv2>%s%s QED %a@]"
+              (step_name qed) (step_dot qed)
               (pp_print_qed_step(*proof_nl*) cx) qed
         | Error msg ->
             fprintf ff "%sERROR (*%s*)" supp msg
diff --git a/src/proof/p_gen.ml b/src/proof/p_gen.ml
index 29a48d92..58062412 100644
--- a/src/proof/p_gen.ml
+++ b/src/proof/p_gen.ml
@@ -267,7 +267,8 @@ let rec generate (sq : sequent) prf time_flag =
             | Elsewhere _ ->
                 ()
           end;
-          prf
+          let ob = obligate (sq @@ prf) (Ob_omitted h) in
+          assign prf Props.obs [ob]
       | Steps (inits, qed) ->
           let (sq, inits, time_flag) = List.fold_left gen_step (sq, [], time_flag) inits in
           let inits = List.rev inits in
@@ -397,7 +398,8 @@ let collect prf =
     inherit [unit] P_visit.map as super
     method proof scx prf =
       let prf = match prf.core with
-        | Obvious | By _ | Error _ ->
+        | Obvious | By _ | Error _ | Omitted _ ->
+            (* The omitted obs will be removed later, they are useful in LSP. *)
             let () = match query prf Props.obs, query prf Props.supp with
               | Some obs, None ->
                   Stats.checked := List.length obs + !Stats.checked ;
@@ -409,8 +411,6 @@ let collect prf =
                   end obs
               | _ -> () in
             prf
-        | Omitted _ ->
-            prf
         | Steps (sts, qed) ->
             let qed_prf = self#proof scx (get_qed_proof qed) in
             let (_, sts) = self#steps scx sts in
diff --git a/src/proof/p_t.ml b/src/proof/p_t.ml
index 92e8ae0c..69c6472d 100644
--- a/src/proof/p_t.ml
+++ b/src/proof/p_t.ml
@@ -16,6 +16,10 @@ let step_number = function
     | Named (n, _, _)
     | Unnamed (n, _) -> n
 
+let sub_step_number (sn : stepno option) : int =
+    match sn with
+    | None -> 1
+    | Some step -> (step_number step) + 1
 
 let string_of_stepno ?(anonid=false) = function
     | Named (sn, sl, _) ->
@@ -78,6 +82,7 @@ type obligation_kind =
     | Ob_main
     | Ob_support
     | Ob_error of string
+    | Ob_omitted of omission
 
 
 type obligation = {
diff --git a/src/proof/p_t.mli b/src/proof/p_t.mli
index b3e868cc..4509f59e 100644
--- a/src/proof/p_t.mli
+++ b/src/proof/p_t.mli
@@ -67,6 +67,7 @@ type obligation_kind =
     | Ob_main
     | Ob_support
     | Ob_error of string
+    | Ob_omitted of omission
 type obligation = {
     id: int option;
     obl: sequent wrapped;
@@ -99,3 +100,4 @@ val get_qed_proof:
     qed_step_ Property.wrapped -> proof
 (* `proof/p_simplify.ml` *)
 val step_number: stepno -> int
+val sub_step_number : stepno option -> int
diff --git a/src/proof/p_visit.ml b/src/proof/p_visit.ml
index 26fc3a34..2a218ac1 100644
--- a/src/proof/p_visit.ml
+++ b/src/proof/p_visit.ml
@@ -187,7 +187,7 @@ class virtual ['hyp] iter = object (self : 'self)
         self#usable scx us
     | Steps (inits, qed) ->
         let scx = self#steps scx inits in
-        self#proof scx (get_qed_proof qed)
+        self#qed scx qed
 
   method steps scx = function
     | [] -> scx
@@ -196,6 +196,9 @@ class virtual ['hyp] iter = object (self : 'self)
         let scx = self#steps scx sts in
         scx
 
+  method qed scx qed =
+    self#proof scx (get_qed_proof qed)
+
   method step scx st =
     let stepnm = string_of_stepno (Property.get st Props.step) in
     let adj_step scx =
diff --git a/src/proof/p_visit.mli b/src/proof/p_visit.mli
index 43fca22c..0222880c 100644
--- a/src/proof/p_visit.mli
+++ b/src/proof/p_visit.mli
@@ -24,6 +24,7 @@ class virtual ['s] iter: object
   method proof: 's scx -> proof -> unit
   method steps: 's scx -> step list -> 's scx
   method step: 's scx -> step -> 's scx
+  method qed: 's scx -> qed_step -> unit
   method usable: 's scx -> usable -> unit
 end
 
diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml
index 4bd57a16..f6affde5 100644
--- a/src/tlapm_lib.ml
+++ b/src/tlapm_lib.ml
@@ -400,6 +400,7 @@ let process_module
         in
         let obs = Array.mapi add_id fin.final_obs in  (* add obligation ids *)
         let obs = toolbox_clean obs in (* only consider specified obligations *)
+        let obs = List.filter (fun ob -> match ob.kind with Ob_omitted _ -> false | _ -> true) obs in
         let fin = {
                 fin with final_obs = Array.of_list obs ;
                 final_status = (Incomplete, summ) } in
diff --git a/src/util/property.ml b/src/util/property.ml
index e0d50763..a02017b4 100644
--- a/src/util/property.ml
+++ b/src/util/property.ml
@@ -86,6 +86,8 @@ let query w pf =
 let assign w pf v =
   { w with props = pf.set v :: List.filter (fun p -> pf.pid <> fst p) w.props }
 
+let with_prop pf v w = assign w pf v
+
 let remove w pf =
   { w with props = List.filter (fun p -> pf.pid <> fst p) w.props }
 
diff --git a/src/util/property.mli b/src/util/property.mli
index 0cb10542..2786823c 100644
--- a/src/util/property.mli
+++ b/src/util/property.mli
@@ -83,6 +83,9 @@ val query  : 'a wrapped -> 'b pfuncs -> 'b option
     doesn't already exist. *)
 val assign : 'a wrapped -> 'b pfuncs -> 'b -> 'a wrapped
 
+(** An [|>] friendly variant of [assign]. *)
+val with_prop : 'b pfuncs -> 'b -> 'a wrapped -> 'a wrapped
+
 (** [remove w pf] removes the property with pid [wf.pid] (if any) from
     [w]. *)
 val remove : 'a wrapped -> 'b pfuncs -> 'a wrapped
diff --git a/src/util/util.ml b/src/util/util.ml
index b91c13ab..e006719b 100644
--- a/src/util/util.ml
+++ b/src/util/util.ml
@@ -38,6 +38,8 @@ module Coll = struct
   module Hs = Set.Make (HC)
 end
 
+module Deque = Deque
+
 let prop : locus pfuncs = make ~uuid:"efa05a42-e82d-40a2-b130-9cfdb089a0d5" "Util.prop"
 
 let get_locus lw = get lw prop
diff --git a/src/util/util.mli b/src/util/util.mli
index 1c7aa632..d28c036f 100644
--- a/src/util/util.mli
+++ b/src/util/util.mli
@@ -9,6 +9,8 @@
 
 open Property
 
+module Deque = Deque
+
 (** {3 Locations} *)
 
 val locate      : 'a -> Loc.locus -> 'a wrapped
diff --git a/tlapm.opam b/tlapm.opam
index 872eb93f..6579b8dc 100644
--- a/tlapm.opam
+++ b/tlapm.opam
@@ -38,7 +38,10 @@ depends: [
   "ppx_inline_test"
   "ppx_assert"
   "ppx_deriving"
-  "ounit2"
+  "ounit2" {with-test}
+  "alcotest" {with-test}
+  "ocolor" {with-test}
+  "patdiff" {with-test}
   "odoc" {with-doc}
 ]
 depopts: ["lsp" "eio_main"]