Suppose $B(x)$ set $(x:A)$ is a family of sets and $D$ is a set. Prove $(\Sigma x:A)B(x) \times D \to (\Sigma x:A)(B(x) \times D)$.
Using the so called Curry-Howard correspondence one may translate this statement into a predicate expression: $(\exists x \phi(x) \land \psi) \to \exists x(\phi(x) \land \psi)$ if $x \not \in \text{FV}(\psi)$. In what follows, I have tried to spell out, as clearly as possible, my incomplete solution to the question.
Subgoal 1: Prove the existence of a derivation in natural deduction of the given expression.
Let $\text{FV}(\exists x \phi(x) \land \psi)=\{z_{1},\dots,z_{k}\}$. My goal then is to show that $\mathfrak{A} \models \forall z_{1} \dots z_{n}\left[(\exists x \phi(x) \land \psi) \to \exists x(\phi(x) \land \psi) \right]$ for all structures $\mathfrak{A}$. Thus, using lemma 2.4.5 (p. 71 Van Dalen) that $\mathfrak{A} \models \exists x[\phi(x, \overline{a}_{1},\dots,\overline{a}_{k}) \land \psi(\overline{a}_{1}, \dots, \overline{a}_{k})] \iff \exists x \phi(x, \overline{a}_{1},\dots,\overline{a}_{k}) \land \psi(\overline{a}_{1}, \dots, \overline{a}_{k})$ for all $\mathfrak{A}$ and all $a_{1}, \dots, a_{k} \in |\mathfrak{A}|$. As $a_{1}, \dots, a_{k}$ remains fixed throughout the argument, I won't -
$\mathfrak{A} \models \exists x \phi(x,----) \land \psi(----) \iff \mathfrak{A} \models \exists x \phi(x,----)$ and $\mathfrak{A} \models \psi(----) \iff \mathfrak{A} \models \phi(\overline{b},----)$ for some $b$ and $\mathfrak{A} \models \psi(----) \iff \phi(\overline{b},----) \land \psi (----)$, for some $b$, $\iff \exists x \left[(\phi(x,----) \land \psi(----)\right]$, which is the desired result. $\mathfrak{Q.E.D}$
By the completeness theorem $\mathfrak{A} \models \Gamma \implies \mathfrak{A} \vdash \Gamma$, there exists a derivation in natural deduction from $(\exists x \phi(x) \land \psi)$ to $\exists x(\phi(x) \land \psi)$ (when $x \not \in \text{FV}(\psi)$).
Subgoal 2: Determine a derivation in natural deduction of $(\exists x \phi(x) \land \psi) \to \exists x(\phi(x) \land \psi)$
I have done so in a proof tree.
Subgoal 3: Translate the derivation obtained in the section above into a type theory
In the case I managed to produce a satisfactory derivation, I now face the somewhat daunting task of translating this into type theory. Here is where I am stuck. I have no problem forming $(\Sigma x:A)B(x) \times D$, instead it is the $\Sigma$-elimination rule (which I suppose I should use?) that brings me trouble. How exactly do I express the right branch of the tree in type theory? Help would be very much appreciated.
I think your proof tree has an error in it: $[\exists x \phi(x)\wedge\psi]$ should really be on top (so there's only one branch), followed by the elimination rule for $\exists$ which gives you the beginning of your current branch $\phi([\bar a/x])\wedge\psi$.
You can get the type-theoretic proof by just replacing all your statements and inferences with their type-theoretic versions that the Curry-Howard isomorphism gives you (this is the point of the Curry-Howard isomorphism: inferences in standard logic correspond exactly to inferences in type theory). Unfortunately, if you try to do any serious back-and-forth between logics without explicitly keeping track of contexts (i.e. lists of free variables), things get harder to see.
To use the type-theoretic elimination rule, you start with $p:(\sum x:A)B(x)\wedge D$, from which you automatically get $\pi_1(p):(\sum x:A)B(x)$ and $\pi_2(p):D$.
Then it is easy to see that the three hypotheses for the elimination rule for $\sum$ are satisfied:
Since the terms of $\sum(x:A)B(x)$ are supposed to be precisely (dependent) pairs of terms $x:A$, $y:B(x)$, then 3. saying that we have such a term, and since 2. says that any such dependent pair of terms gives us a term of what we want to prove, we should be able to build a term of our conclusion. This is exaftly what the elimination rule for $\sum$ says we can do! So we get: