Interesting, the notation used in that paper presages the notation used by TLA⁺² [1]. I actually have written up an exposition of TLA⁺² proof steps using seque

Interesting, the notation used in that paper presages the notation used by TLA⁺² [1]. I actually have written up an exposition of TLA⁺² proof steps using sequent calculus notation [2] with the intention of writing a proof visualizer for it. [1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T... [2] https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-reference https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-ref...