Natural deduction proof for $\exists x(\exists y A(y) \rightarrow A(x))$ I spent a long time trying to find a natural deduction derivation for the formula $\exists x(\exists y A(y) \rightarrow A(x))$, but I always got stuck at some point with free variables in the leaves. Could someone please help me or give me some hints to find a proof. 
Thanks.
 A: You can derive it this way:


*

*$\exists y\,A(y) \qquad\qquad\textsf{assumption}$

*$A(a) \qquad\quad\qquad\textsf{$\exists$ new parameter introduction}\text{ ($a$)}$

*$\exists y\,A(y) \to A(a) \quad\quad\textsf{discharge 1.}$

*$\exists x\,(\exists y\,A(y) \to A(x)) \quad\textsf{$\exists$ introduction}$

A: If you prefer the tree style notation this is a valid proof:
$$\dfrac{\dfrac{\lower{1.5ex}{[\exists y~A(y)]^1}~~\dfrac{[A(s)]^2}{A(s)}{}}{\dfrac{A(s)}{\exists y~A(y)~\to~A(s)}{(\to i,1)}}{(\exists e,1)}}{\exists x~(\exists y~A(y)~\to~A(x))}{(\exists i)}$$
A: The following is a natural deduction proof of the formula $\exists x (\exists y A(y) \rightarrow A(x))$
$$
\dfrac
{
  \dfrac
  {
    \dfrac
    {
      \dfrac
      {
        \dfrac
        {
          \dfrac
          {}
          {
            [\exists y A(y)]_2
          } 
          \dfrac
          {
            \dfrac
            {
              \dfrac
              {
                \dfrac{\dfrac{}{[A(b)]_3}}{\exists y A(y) \rightarrow A(b)} \rightarrow_i
              }
              { 
                \exists x (\exists y A(y) \rightarrow A(x))
              } \exists_i
              \dfrac{}{[\neg \exists x (\exists y \rightarrow A(x))]_1}
            }
            {\bot} \neg_e
          }
          {
            A(x)
          } \bot_e
        }
        {
          A(x)
        } \exists_{e,3}
      }
      {
        \exists y A(y) \rightarrow A(x)
      } \rightarrow_{i,2}
    }
    {
      \exists x (\exists y A(y) \rightarrow A(x))
    }
    \dfrac{}{[\neg \exists x(\exists y A(y) \rightarrow A(x))]_1}
  }
  {
    \bot
  } \neg_e
}
{
  \exists x (\exists y A(y) \rightarrow A(x))
} \mathrm{RAA_1}
$$
Since the formula $\exists x(\exists y A(y) \rightarrow A(x))$ is not valid in intuitionistic logic, it can not be proven in this natural deduction system without the rule RAA (or the rule DNE).
