proof


\documentclass[tikz,border=5mm]{standalone}
\usetikzlibrary{positioning}
\usetikzlibrary{backgrounds}
\usetikzlibrary{arrows}
\usetikzlibrary{shapes,shapes.geometric,shapes.misc}

\begin{document}

\pgfdeclarelayer{edgelayer}
\pgfdeclarelayer{nodelayer}
\pgfsetlayers{background,edgelayer,nodelayer,main}

\tikzstyle{brace}=[decorate, decoration=calligraphic brace]
\tikzstyle{boxed}=[fill=white, draw=black, shape=rectangle]
\tikzstyle{none}=[inner sep=0mm]

\begin{tikzpicture}[baseline=-0.25em,scale=0.5]
	\begin{pgfonlayer}{nodelayer}
		\node [style=none] (0) at (1, 0.25) {$(q,w)\vdash_{M_I}^* (p,\lambda)$};
		\node [style=none] (1) at (1, -1) {$\Downarrow$};
		\node [style=none] (2) at (-4.75, -2.25) {$(q,va)$};
		\node [style=none] (3) at (-2.75, -2.25) {$\vdash_{M_I}^*$};
		\node [style=none] (4) at (-1, -2.25) {$(r_1,a)$};
		\node [style=none] (5) at (2.75, -2.25) {$(r_2,\lambda)$};
		\node [style=none] (6) at (1, -2.25) {$\vdash_{M_I}$};
		\node [style=none] (7) at (4.75, -2.25) {$\vdash_{M_I}^*$};
		\node [style=none] (8) at (6.5, -2.25) {$(p,\lambda)$};
		\node [style=none] (10) at (-8, -5.75) {$(q,v)\vdash_{M_I}^*(r_1, \lambda)$};
		\node [style=none] (12) at (0.75, -6.75) {$r_2\in\Delta(r_1,a)$};
		\node [style=none] (14) at (7, -5.5) {$p\in\Lambda(r_2)$};
		\node [style=none] (15) at (0.75, -7.75) {$\Downarrow$};
		\node [style=none] (16) at (0.75, -9) {$\Lambda(r_2)\subseteq\delta(R_1,a)$};
		\node [style=none] (17) at (-8, -7) {$\Downarrow$};
		\node [style=none] (18) at (-8, -8.25) {$(\Lambda(q),v)\vdash_{M_D}^*(R_1, \lambda)$};
		\node [style=none] (19) at (-8, -9) {\tiny amb $R_1\subseteq \mathcal{P}(k)$};
		\node [style=none] (20) at (-8, -9.5) {\tiny tal que $r_1\in R_1$};
		\node [style=none] (21) at (-9.25, -7) {\tiny (H.I.)};
		\node [style=none] (22) at (-8, -10.5) {$\Downarrow$};
		\node [style=none] (23) at (-8, -11.75) {$(\Lambda(q),va)\vdash_{M_D}^*(R_1, a)$};
		\node [style=none] (24) at (-2.75, -3.5) {};
		\node [style=none] (25) at (-8, -5) {};
		\node [style=none] (26) at (-8, -5.75) {};
		\node [style=none] (27) at (1, -4.5) {};
		\node [style=none] (28) at (0.75, -6) {};
		\node [style=none] (29) at (4.75, -3.5) {};
		\node [style=none] (30) at (7, -4.75) {};
		\node [style=none] (31) at (-6, -3) {};
		\node [style=none] (32) at (0, -3) {};
		\node [style=none] (33) at (-2, -3.75) {};
		\node [style=none] (34) at (3.75, -3.75) {};
		\node [style=none] (35) at (1.75, -3) {};
		\node [style=none] (36) at (7.25, -3) {};
		\node [style=none] (37) at (-2.75, -3.25) {};
		\node [style=none] (38) at (1, -4) {};
		\node [style=none] (39) at (4.75, -3.25) {};
		\node [style=none] (40) at (-2.25, -9.5) {};
		\node [style=none] (41) at (8.5, -9.5) {};
		\node [style=none] (42) at (3.5, -10) {};
		\node [style=none] (43) at (7, -6) {};
		\node [style=none] (44) at (7, -9.25) {};
		\node [style=none] (45) at (3.5, -10.75) {$\Downarrow$};
		\node [style=none] (46) at (3.5, -11.75) {$p\in\delta(R_1,a)$};
		\node [style=none] (47) at (3.5, -13) {$\Downarrow$};
		\node [style=none] (48) at (3.5, -14) {$(R_1, a) \vdash_{M_D}(P,\lambda)$};
		\node [style=none] (49) at (3.5, -14.75) {\tiny per algun $P\subseteq \mathcal{P}(k)$};
		\node [style=none] (50) at (3.5, -15.25) {\tiny tal que $p\in P$};
		\node [style=none] (51) at (-11, -16) {};
		\node [style=none] (52) at (9.5, -15.75) {};
		\node [style=none] (53) at (-0.5, -16.75) {};
		\node [style=none] (54) at (-0.5, -17.5) {$\Downarrow$};
		\node [style=boxed] (55) at (-0.5, -18.75) {$\left(\Lambda(q),va\right)\vdash_{M_D}^*(R_1, a)\vdash_{M_D}(P,\lambda)$};
		\node [style=none] (56) at (-8, -12.5) {};
		\node [style=none] (57) at (-8, -16) {};
		\node [style=none] (58) at (2.25, -7.5) {\tiny consturcció};
		\node [style=none] (59) at (-6.75, -7) {\tiny $|v|=k$};
		\node [style=none] (60) at (2.25, -7.75) {\tiny de $\delta$};
	\end{pgfonlayer}
	\begin{pgfonlayer}{edgelayer}
		\draw [style=none, in=90, out=-75, looseness=0.75] (24.center) to (25.center);
		\draw [style=none, in=90, out=-90] (27.center) to (28.center);
		\draw [style=none, in=90, out=-90] (29.center) to (30.center);
		\draw [in=90, out=-90, looseness=0.25] (31.center) to (37.center);
		\draw [in=-90, out=90, looseness=0.25] (37.center) to (32.center);
		\draw [in=90, out=-90, looseness=0.25] (33.center) to (38.center);
		\draw [in=-90, out=90, looseness=0.25] (38.center) to (34.center);
		\draw [in=90, out=-90, looseness=0.25] (35.center) to (39.center);
		\draw [in=-90, out=90, looseness=0.25] (39.center) to (36.center);
		\draw [in=90, out=-90, looseness=0.25] (40.center) to (42.center);
		\draw [in=-90, out=90, looseness=0.25] (42.center) to (41.center);
		\draw [style=none] (43.center) to (44.center);
		\draw [in=90, out=-90, looseness=0.25] (51.center) to (53.center);
		\draw [in=-90, out=90, looseness=0.25] (53.center) to (52.center);
		\draw [style=none] (56.center) to (57.center);
	\end{pgfonlayer}
\end{tikzpicture}
\end{document}