Quantification in the infer command of the proof package

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

enter image description here


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.

enter image description here

\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>}:

enter image description here

\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}