\documentclass[a3paper,landscape]{scrartcl}
\usepackage{proof}
\usepackage[left=0mm]{geometry}

% Needed commands:
%
% 1) infer command ([rule] can be omitted)
%
% \infer[rule]{ conclusion }{ premise1 & premise2 & ... premisen }
%
% 2) \textrm{ text } -- display normal text in math mode
%
% 3) \\   -- newline command
%
% Modes: 
%  inline math mode:
%  $ ... $
%
%  "longer" (on its own line and sometimes in bigger font) math mode: 
%  \[ ... \]
%
% Symbols: 
%   \alpha \beta \gamma ...
%   \Rightarrow \rightarrow 
%   \equiv = + - * / 
%


\begin{document}
\[
  \infer[Op]{\textrm{dbl(5) = inv(dbl(inv 5))} \Rightarrow \textrm{true}}{
	  \infer[App]{\textrm{dbl(5)} \Rightarrow 10}{\textrm{dbl} \Rightarrow \textrm{fun } x \rightarrow 2 * x & 5 \rightarrow 5 & (2 * x)[5/x] \Rightarrow 10}
	  \infer[App]{\textrm{inv(dbl(inv 5))} \Rightarrow 10}{
		  \textrm{inv} \Rightarrow \textrm{fun } y \rightarrow -y & 
		  \infer[App]{\textrm {dbl (inv 5)} \Rightarrow -10}{
			  \textrm{dbl} \Rightarrow \textrm{fun } x \rightarrow 2 * x &
			  \infer[App]{\textrm{inv } 5 \Rightarrow 5}{
				  \textrm{inv} \Rightarrow \textrm{fun }y \rightarrow -y &
				  5 \Rightarrow 5 &
				  -y[5/y] \Rightarrow -5}
			  &
			  (2 * x)[-5/x] \Rightarrow -10
			  }
		  &
		  -y[-10/y] \Rightarrow 10}
	  & 10 \Rightarrow 10
	  }
\]
\end{document}
