eqnarray directly in sproof impossible

[kohlhase]

It seems currently impossible to have an eqnarry* directly inside an sproof environment. See MathHub/MiKoMH/CompLog/source/stlc/mod/abe-sound.en.tex, where I have fixed this via an additional \spfstep.

      \spfstep{
        \begin{eqnarray*}
        \appo{\Evaluation\phi{\lamcdot{Y}{{\sbst{Y}{X}}\bA}}}\sema 
        & = & \Evaluation{\sbstExtend\phi{\sbst{a}{Y}}}{\sbstApply{\sbst{Y}{X}}\bA}\\
        & = & \Evaluation{\sbstExtend\phi{\sbst{a}{X}}}\bA\\
        & = & \appo{\Evaluation\phi{\lamcdot{X}\bA}}\sema
      \end{eqnarray*}}

But this is not very nice, we should have something better (yes, I know that there is \spfstep* that is a bit less intrusive, but that does not really help the underlying problem).

Either a replacement for the eqnarray* (that I only had to introduce since the old {spfeq} environment got deleted BTW), that allows to mark up the "steps" in the equational proof somehow semantically, ... or ... don't really know.

Actually,abe-sound.en.tex is the only place where I had {spfeq} in the sources.

[kohlhase]

Also note the justification construction in the second frame (third line):

    \begin{sproof}[for=eta-sound,id=eta-sound-pf]{by calculation}
      \spfstep*{\begin{eqnarray*}
      \appo{\Evaluation\phi{\lamcdot{X}{\apply[lambda]\bA{X}}}}\sema 
      & = & \Evaluation{\sbstExtend\phi{\sbst{\sema}{X}}}{\apply[lambda]\bA{X}}\\
      & = & \appo{\Evaluation{\sbstExtend\phi{\sbst{\sema}{X}}}\bA}{\Evaluation{\sbstExtend\phi{\sbst{\sema}{X}}}{X}}\\
      & = & \appo{\Evaluation\phi\bA}{\Evaluation{\sbstExtend\phi{\sbst{\sema}{X}}}{X}} \qquad
            \text{as $\ninset{X}{\freevars\bA}$.}\\
      & = & \appo{\Evaluation\phi\bA}\sema
      \end{eqnarray*}}
    \end{sproof}

[Jazzpirate]

If you actually have a new line for every new derivation step, it seems to me like \eqstep perfectly subsumes that (I think it's not well documented yet). Apart from that, \begin{spfblock} is the most "neutral" variant of putting arbitrary text in a proof (e.g. eqnarray), and should still allo for proofsteps, yield etc, just making them presentationally neutral