Identical spacing of inference lines with Bussproofs

Question

I'd like every derivation in my document to meet these two requirements:

1. The distance between two consecutive inference lines should always be the same (the red arrows in the figure should have equal length).
2. The thesis symbol should be vertically centered with respect to the superior and inferior inference lines (the blue lines in the figure should have equal length).

MWE:

\documentclass{article}

\usepackage{amsmath}
\usepackage{tikz}
\usepackage{bussproofs}
\usepackage{bussproofs-extra}

\begin{document}
 \begin{center}
  \AxiomC{}
  \UnaryInfC{$B \vdash B$}
  \UnaryInfC{$\vdash A,B$}
  \UnaryInfC{$\neg A \vdash B$}
  \AxiomC{}
  \RightLabel{$\pi_0$}
  \DeduceC{$B \vdash \lVert A\rVert$}
  \RightLabel{\scriptsize$(\mathit{cut})$}
  \BinaryInfC{$\neg A \vdash \lVert A\rVert$}
  \DisplayProof
 \end{center}
\end{document}

Answer 1

Without knowing the bussproofs package, I'd suggest that you switch off the standard interlineskip and include a "strut" in every inference.

In plain TeX, you can use \offinterlineskip in tables if you want to control the line height via struts. Is there something analogous in bussproofs?

The strut is defined and used as follows:

\def\infcstrut{\vrule width 0pt height Xpt depth Ypt} % once at the beginning
...
\UnaryInfC{$\infcstrut B \vdash B$}

Here Y is a number large enough to accomodate the \lVert that goes below the baseline in the third row, and X = Y + height of thesis symbol.

Addendum: After looking briefly at the bussproof source code, I am sorry to say that this package seems to have its own detailed rules for calculating the distance between lines, which should not be so easy to override.

2nd addendum: Here's what I meant, done in plain TeX. (But that isn't easily generalizable, I'm afraid.)

\hsize 12em
\def\mystrut{\vrule width0pt height10.444pt depth3.5pt}
\def\label{\leaders\vbox to.75ex{\hsize=.25\hsize\line{\hss.}}\vfil}
\def\infc#1{\mystrut\hss$#1$\hss}
\offinterlineskip
\leftline{\valign{&\hrule #&\hbox to.5\hsize{\infc{#}}\cr
&B\vdash B&&\vdash A,B&height.75pt&\neg A \vdash B\cr
\multispan5{\label}&B \vdash \Vert A\Vert\cr
\multispan5{\vss\hbox to0pt{\hskip -.25\hsize$\;\pi_0$\hss}\vss}\cr
}}
\vbox to0pt{\vss\line{\hss\rlap{$\;(cut)$}}\vss}
\hrule
\line{\infc{\neg A \vdash \Vert A\Vert}}
\bye

Answer 2

(Not a solution, simply an attempt.)

I don't think this is realistically achievable, but I feel that if a solution exists, you would have better chances of finding it with ebproof.

\documentclass{article}
\usepackage{amsmath}
\usepackage{ebproof}
\begin{document}
\begin{center}
    \begin{prooftree}[
        rule margin=0pt,     % Spacing above and below inference lines set to 0.
        rule code={          % This code replaces the code for the inference line with…
            \vspace{.2em}    % … a space above the line…
            \hrule           % … the line itself …
            \vspace{.3em}    % … a space below the line.
        }
        ]  
        \hypo{}
        \infer1{B \vdash B}
        \infer1{\vdash A,B}
        \infer1{\neg A \vdash B}
        \hypo{}
        \ellipsis{\(\pi_0\)}{B \vdash \lVert A\rVert}
        \infer2[\((\mathit{cut})\)]{\neg A \vdash \lVert A\rVert}
    \end{prooftree}
\end{center}
\end{document}

gives:

It looks a bit nicer (both in the code and in the appearance, if you ask me) than what you have right now.

(The idea of using a struct, now abandoned, comes from https://tex.stackexchange.com/a/614725/34551 but does not seem to achieve what I wanted, i.e. a fixed line height)