Type Theory (Proof tree) 
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.
 A: 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:


*

*$p:(\sum x:A)B(x)\wedge D\vdash (\sum x:A) (B(x)\wedge D)$ Type (this just says that what we are trying to prove is well-formed)

*$p:(\sum x:A)B(x)\wedge D,\, a:A, b:B(a)\vdash (a,(b,\pi_2(p)):(\sum x:A) (B(x)\wedge D)$ (this says that if we had our initial assumption, and terms $a:A$ and $b:B(a)$, then we have a term of $(\sum x:A)(B(x)\wedge D)$, which is true by term-introduction first for $\wedge$, and then for $\sum$

*$p:(\sum x:A)B(x)\wedge D\vdash \pi_1(p): \sum(x: A)B(x):$ (this says that we do in fact have a term of $\sum(x: A)B(x)$ under our assumption) 


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:


*

*$p:(\sum x:A)B(x)\vdash ind_{(\sum x:A):B)}(x.y.(y,\pi_2(p)),p):\sum(x:A)(B(x)\wedge D)$

