# Quantification in the infer command of the proof package

I'm trying to write this inference rule using the infer command of the proof package:

For that I'm using the command:

$\infer{s = s'}{% R \subseteq A^{\omega} \times A^{\omega} & R \; s \; s' & \forall s_1, s_2. \infer{\text{head}(s_1) = \text{head}(s_2) \land R(\text{tail}(s_1), \text{tail}(s_2))}{% R \; s_1 \; s_2 } }$


However, the forall quantification appears in the lower level as:

How can I put it in the middle like above?

• You may use \operatorname{} instead of \text{} – user94293 Nov 14 at 21:28

I propose a \qinfer command:

\documentclass{article}

\usepackage{proof,amsmath}

\newcommand{\func}[1]{\mathrm{#1}}

\newcommand{\qinfer}[3]{%
\sbox0{\infer{#2}{#3}}%
\raisebox{\dimexpr(\ht0-1ex)/2}{$#1\;$}%
\box0
}

\begin{document}

$\infer{s = s'}{% R \subseteq A^{\omega} \times A^{\omega} & R \; s \; s' & \qinfer{\forall s_1,s_2} {\func{head}(s_1) = \func{head}(s_2) \land R(\func{tail}(s_1), \func{tail}(s_2))} {R \; s_1 \; s_2} }$

\end{document}


I also fixed \text into \mathrm, which is the correct command to use here (if not \operatorname).

The name of the inference rule can be added as an optional argument to \infer:

\infer[label]{conclusion}{premises}


However, the label is added to the right.

\documentclass{article}
\usepackage{proof}
\usepackage{amsmath}
\begin{document}
$\infer{s = s'}{% R \subseteq A^{\omega} \times A^{\omega} & R \; s \; s' & \infer[\forall s_1, s_2]{% \text{head}(s_1) = \text{head}(s_2) \land R(\text{tail}(s_1), \text{tail}(s_2))% }{% R \; s_1 \; s_2 } }$
\end{document}


You can raise this into position using \raisebox{<len>}{<stuff>}:

\documentclass{article}

\usepackage{proof,amsmath}

\begin{document}

$\infer{s = s'}{% R \subseteq A^{\omega} \times A^{\omega} & R \; s \; s' & \raisebox{.6\baselineskip}{\forall s_1, s_2~} \infer{\text{head}(s_1) = \text{head}(s_2) \land R(\text{tail}(s_1), \text{tail}(s_2))}{% R \; s_1 \; s_2 } }$

\end{document}