Formula in premise overflows derivation line using bussproofs

Question

I came to

the universally quantified assumption overflows the derivation line.

My source is

\documentclass{beamer}
\usepackage{bussproofs}

\newcommand{\mydots}{
\def\extraVskip{-2pt}
\noLine
\UnaryInfC{\vdots}
\def\extraVskip{2pt}
\noLine
}

\begin{document}

\AxiomC{$\exists t. A(t)$}
\AxiomC{[$\forall t. A(t)$]}
\mydots
\UnaryInfC{$C$}
\RightLabel{$\exists$E}
\BinaryInfC{$C$}
\DisplayProof

\end{document}

How can I fix this within using bussproofs.sty ?

Answer 1

I believe it's a precise choice of bussproofs as the examples on page 4 show: here's one

You can tell it to use the same width as a previous item with a box:

\documentclass{beamer}
\usepackage{calc}
\usepackage{bussproofs}

\newcommand{\mydots}{%
  \noLine
  \UnaryInfC{\vphantom{\ensuremath{X}}\smash{\vdots}}%
  \noLine
}

\begin{document}

\begin{frame}

\AxiomC{$\exists t. A(t)$}
\AxiomC{[$\forall t. A(t)$]}
\mydots
\UnaryInfC{\makebox[\widthof{[$\forall t. A(t)$]}]{$C$}}
\RightLabel{$\exists$E}
\BinaryInfC{$C$}
\DisplayProof

\end{frame}

\end{document}