package bussproofs per albero di derivazione

Salve, ho il seguente problema
devo fare un albero di deduzione ma ho 2 problemi:

1. siccome le premesse sono lunghissime allora le spezzo su più righe e le allineo con \fCenter (come da manuale della classe)
a me servono allineate a sinistra e allora inserisco tutto a destra del comando, però poi quando devo allineare al “vero” centro sevo mette un sacco di \quad per allineare.
Esiste un modo migliore?

2. quando scarico una premessa vorrei inserirla tra parentesi quadrate, finché sono su una sola riga non c’è problema, ma quando sono su più righe c’è un modo per allargare le parentesi a tutta la premessa?

Il codice è il seguente:
`
\documentclass[a4paper,10pt]{article}
\usepackage[italian]{babel}

\usepackage[utf8]{inputenc}
\usepackage{amssymb, amsmath}
\usepackage{amsthm}
\usepackage{bussproofs} % per alberi di deduzione naturale

\begin{document}
\begin{prooftree}
\def\fCenter{}
\AxiomC{$[S_0']^2$}
\AxiomC{$F$}
\Axiom$[\fCenter \forall A' \forall F' \forall G' \forall K.$
\def\extraVskip{0pt}
\noLine
\UnaryInf$\fCenter (\;(F' \to S_0'(A', F'))$
\noLine
\UnaryInf$\fCenter \;\;\land ((S_0'(A', F') \land S_0'(A', (F' \to G'))) \to S_0'(A', G'))$
\noLine
\UnaryInf$\fCenter \;\;\land (K\; \mbox{signed}\; F' \to S_0'(\mbox{name}(K), F'))\;)]^1\quad\quad\quad\quad$
\def\extraVskip{2pt}
\RightLabel{\footnotesize $\land E_l$}
\UnaryInf$\fCenter (\;(F \to S_0'(A, F))$
\def\extraVskip{0pt}
\noLine
\UnaryInf$\fCenter \;\;\land ((S_0'(A, F) \land S_0'(A, (F \to G))) \to S_0'(A, G))$
\noLine
\UnaryInf$\fCenter \;\;\land (K\; \mbox{signed}\; F \to S_0'(\mbox{name}(K), F))\;)$
\def\extraVskip{2pt}
\RightLabel{\footnotesize $\land E_l$}
\UnaryInf$\fCenter \quad\quad\quad\quad\quad\quad F \to S_0'(A, F)$
\RightLabel{\footnotesize $\to E$}
\BinaryInf$\fCenter \quad S_0'(A, F)$
\RightLabel{\footnotesize $\to I^1$}
\UnaryInf$\fCenter \forall A' \forall F' \forall G' \forall K.$
\def\extraVskip{0pt}
\noLine
\UnaryInf$\fCenter (\;(F' \to S_0'(A', F'))$
\noLine
\UnaryInf$\fCenter \;\;\land ((S_0'(A', F') \land S_0'(A', (F' \to G'))) \to S_0'(A', G'))$
\noLine
\UnaryInf$\fCenter \;\;\land (K\; \mbox{signed}\; F' \to S_0'(\mbox{name}(K), F'))\;)\quad\quad\quad\quad$
\noLine
\UnaryInf$\fCenter \to S_0'(A, F) \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad $
\def\extraVskip{2pt}
\RightLabel{\footnotesize $\forall_{S'} I^2$}
\BinaryInfC{def. \mbox{A} \mbox{says} \mbox{F}}
\end{prooftree}
\end{document}
`

Grazie.