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?
\operatorname{}
instead of\text{}
– user94293 Nov 14 '19 at 21:28