% These definitions - the "preable" of a .dnt file - are from:
%   http://angg.twu.net/dednat5/preamble.lua.html
%   http://angg.twu.net/dednat5/preamble.lua
%                    (find-dn5 "preamble.lua")
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}
\def\ifdedundefined#1{\expandafter\ifx\csname ded-#1\endcsname\relax}
\def\ded#1{\ifdedundefined{#1}
    \errmessage{UNDEFINED DEDUCTION: #1}
  \else
    \csname ded-#1\endcsname
  \fi
}
\def\defdiag#1#2{\expandafter\def\csname diag-#1\endcsname{\bfig#2\efig}}
\def\defdiagprep#1#2#3{\expandafter\def\csname diag-#1\endcsname{{#2\bfig#3\efig}}}
\def\ifdiagundefined#1{\expandafter\ifx\csname diag-#1\endcsname\relax}
\def\diag#1{\ifdiagundefined{#1}
    \errmessage{UNDEFINED DIAGRAM: #1}
  \else
    \csname diag-#1\endcsname
  \fi
}
% End of the preamble.


\defdiag{foo}{ % no hyperlink yet
  \morphism(0,0)/<=/<300,0>[{a,b}`{a};]
  \morphism(0,0)/|->/<0,-300>[{a,b}`{c};]
  \morphism(300,0)/|->/<0,-300>[{a}`{b\mapsto c};]
  \morphism(0,-300)/=>/<300,0>[{c}`{b\mapsto c};]
}
\defded{f(1+2+3)}{
 \infer[{ababc}]{ \mathstrut f(1+2+3) }{
  \infer=[{}]{ \mathstrut 1+2+3 }{
   \mathstrut 1 &
   \mathstrut 2 &
   \mathstrut 3 } } }