add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
\ProvidesPackage{proof}[1995/05/22]
% proof.sty (Proof Figure Macros)
%
% version 2.0
% June 24, 1991
% Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
%
%Modified for LaTeX-2e by L. C. Paulson
%
% This program is free software; you can redistribute it or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either versions 1, or (at your option)
% any later version.
%
% This program is distributed in the hope that it will be useful
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details.
%
% Usage:
% In \documentstyle, specify an optional style `proof', say,
% \documentstyle[proof]{article}.
%
% The following macros are available:
%
% In all the following macros, all the arguments such as
% <Lowers> and <Uppers> are processed in math mode.
%
% \infer<Lower><Uppers>
% draws an inference.
%
% Use & in <Uppers> to delimit upper formulae.
% <Uppers> consists more than 0 formulae.
%
% \infer returns \hbox{ ... } or \vbox{ ... } and
% sets \@LeftOffset and \@RightOffset globally.
%
% \infer[<Label>]<Lower><Uppers>
% draws an inference labeled with <Label>.
%
% \infer*<Lower><Uppers>
% draws a many step deduction.
%
% \infer*[<Label>]<Lower><Uppers>
% draws a many step deduction labeled with <Label>.
%
% \infer=<Lower><Uppers>
% draws a double-ruled deduction.
%
% \infer=[<Label>]<Lower><Uppers>
% draws a double-ruled deduction labeled with <Label>.
%
% \deduce<Lower><Uppers>
% draws an inference without a rule.
%
% \deduce[<Proof>]<Lower><Uppers>
% draws a many step deduction with a proof name.
%
% Example:
% If you want to write
% B C
% -----
% A D
% ----------
% E
% use
% \infer{E}{
% A
% &
% \infer{D}{B & C}
% }
%
% Style Parameters
\newdimen\inferLineSkip \inferLineSkip=2pt
\newdimen\inferLabelSkip \inferLabelSkip=5pt
\def\inferTabSkip{\quad}
% Variables
\newdimen\@LeftOffset % global
\newdimen\@RightOffset % global
\newdimen\@SavedLeftOffset % safe from users
\newdimen\UpperWidth
\newdimen\LowerWidth
\newdimen\LowerHeight
\newdimen\UpperLeftOffset
\newdimen\UpperRightOffset
\newdimen\UpperCenter
\newdimen\LowerCenter
\newdimen\UpperAdjust
\newdimen\RuleAdjust
\newdimen\LowerAdjust
\newdimen\RuleWidth
\newdimen\HLabelAdjust
\newdimen\VLabelAdjust
\newdimen\WidthAdjust
\newbox\@UpperPart
\newbox\@LowerPart
\newbox\@LabelPart
\newbox\ResultBox
% Flags
\newif\if@inferRule % whether \@infer draws a rule.
\newif\if@DoubleRule % whether \@infer draws doulbe rules.
\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
\newif\if@MathSaved % whether inner math mode where \infer or
% \deduce appears.
% Special Fonts
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
% Math Save Macros
%
% \@SaveMath is called in the very begining of toplevel macros
% which are \infer and \deduce.
% \@RestoreMath is called in the very last before toplevel macros end.
% Remark \infer and \deduce ends calling \@infer.
%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
\def\@SaveMath{}
\def\@RestoreMath{}
% Macros
\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
\ifx \@tempa \@tempb #2\else #3\fi }
\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
\@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
\@ifnextchar [{\@infer}{\@infer[\@empty]}}
\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
\@ifnextchar [{\@infer}{\@infer[\@empty]}}
\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
{\@inferRulefalse \@infer[\@empty]}}
% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
\def\@deduce#1[#2]#3#4{\@inferRulefalse
\@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
% \@infer[<Label>]<Lower><Uppers>
% If \@inferRuletrue, it draws a rule and <Label> is right to
% a rule. In this case, if \@DoubleRuletrue, it draws
% double rules.
%
% Otherwise, draws no rule and <Label> is right to <Lower>.
\def\@infer[#1]#2#3{\relax
% Get parameters
\if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
\setbox\@LabelPart=\hbox{$#1$}\relax
\setbox\@LowerPart=\hbox{$#2$}\relax
%
\global\@LeftOffset=0pt
\setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
\global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
\inferTabSkip
\global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
#3\cr}}\relax
% Here is a little trick.
% \@ReturnLeftOffsettrue(false) influences on \infer or
% \deduce placed in ## locally
% because of \@SaveMath and \@RestoreMath.
\UpperLeftOffset=\@LeftOffset
\UpperRightOffset=\@RightOffset
% Calculate Adjustments
\LowerWidth=\wd\@LowerPart
\LowerHeight=\ht\@LowerPart
\LowerCenter=0.5\LowerWidth
%
\UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
\advance\UpperWidth by -\UpperRightOffset
\UpperCenter=\UpperLeftOffset
\advance\UpperCenter by 0.5\UpperWidth
%
\ifdim \UpperWidth > \LowerWidth
% \UpperCenter > \LowerCenter
\UpperAdjust=0pt
\RuleAdjust=\UpperLeftOffset
\LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
\RuleWidth=\UpperWidth
\global\@LeftOffset=\LowerAdjust
%
\else % \UpperWidth <= \LowerWidth
\ifdim \UpperCenter > \LowerCenter
%
\UpperAdjust=0pt
\RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
\LowerAdjust=\RuleAdjust
\RuleWidth=\LowerWidth
\global\@LeftOffset=\LowerAdjust
%
\else % \UpperWidth <= \LowerWidth
% \UpperCenter <= \LowerCenter
%
\UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
\RuleAdjust=0pt
\LowerAdjust=0pt
\RuleWidth=\LowerWidth
\global\@LeftOffset=0pt
%
\fi\fi
% Make a box
\if@inferRule
%
\setbox\ResultBox=\vbox{
\moveright \UpperAdjust \box\@UpperPart
\nointerlineskip \kern\inferLineSkip
\if@DoubleRule
\moveright \RuleAdjust \vbox{\hrule width\RuleWidth
\kern 1pt\hrule width\RuleWidth}\relax
\else
\moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
\fi
\nointerlineskip \kern\inferLineSkip
\moveright \LowerAdjust \box\@LowerPart }\relax
%
\@ifEmpty{#1}{}{\relax
%
\HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
\advance\HLabelAdjust by -\RuleWidth
\WidthAdjust=\HLabelAdjust
\advance\WidthAdjust by -\inferLabelSkip
\advance\WidthAdjust by -\wd\@LabelPart
\ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
%
\VLabelAdjust=\dp\@LabelPart
\advance\VLabelAdjust by -\ht\@LabelPart
\VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
\advance\VLabelAdjust by \inferLineSkip
%
\setbox\ResultBox=\hbox{\box\ResultBox
\kern -\HLabelAdjust \kern\inferLabelSkip
\raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
%
}\relax % end @ifEmpty
%
\else % \@inferRulefalse
%
\setbox\ResultBox=\vbox{
\moveright \UpperAdjust \box\@UpperPart
\nointerlineskip \kern\inferLineSkip
\moveright \LowerAdjust \hbox{\unhbox\@LowerPart
\@ifEmpty{#1}{}{\relax
\kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
\fi
%
\global\@RightOffset=\wd\ResultBox
\global\advance\@RightOffset by -\@LeftOffset
\global\advance\@RightOffset by -\LowerWidth
\if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
%
\box\ResultBox
\@RestoreMath
}
\endinput