Quantification in the infer command of the proof package

Question

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?

Answer 1

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).

Answer 2

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}

Answer 3

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}