Equivalent Definitions of Types In my reading, I have seen two different definitions of an $n$-types which I think are equivalent, but I am stuck in showing this. 
First I will fix notation:
Let $\mathcal{M}$ be an $\mathcal{L}$-structure and let $A\subseteq M$. Define $\mathcal{L}_A$ to be the language obtained by adding a new constant $c_a$ to $\mathcal{L}$ for each $a\in A$. One can naturally view $\mathcal{M}$ as an $\mathcal{M}_A$-structure by interpreting $c_a$ in the obvious way for each $a\in A$. Define $\text{Th}_A(\mathcal{M})$ to be $\text{Th}(\mathcal{M})$, where $\mathcal{M}$ is viewed as an $\mathcal{L}_A$-structure, and where
$$\text{Th}(\mathcal{M})=\{\varphi \; | \; \varphi \; \text{is an} \; \mathcal{L}\text{-sentence and} \; \mathcal{M}\models \varphi\}.$$ 
Definition 1: Let $p$ be a set of $\mathcal{L}_A$-formulas in free variable $\{v_1,\cdots,v_n\}$. $p$ is called an $n$-type if $p\cup \text{Th}_A(\mathcal{M})$ is satisfiable. 
Definition 2: Let $p$ be a set of $\mathcal{L}_A$-formulas in free variable $\{v_1,\cdots,v_n\}$.$p$ is an $n$-type if, for every finite subset $\Delta$ of $p$, there is some $(m_1,\cdots,m_n)\in M^n$ which simultaneously realize $\Delta$. 
I have made some progress, but I am unsure whether or not this is a workable approach:
Assume $p$ satisfies definition 1. Then $p\cup \text{Th}_A(\mathcal{M})$ is satisfiable. By the compactness theorem, this happens if and only if every finite subset $\Delta$ is satisfiable. We can assume $\Delta$ consists only of elements of $p$. Suppose $\Delta=\{\varphi_1(\overline{v}),\cdots,\varphi_k(\overline{v})\}$, where $\overline{v}=(v_1,\cdots,v_n)$. Let $\psi(\overline{v})=\varphi_1(\overline{v})\wedge \cdots \wedge\varphi_k(\overline{v})$. Now, by the completeness of $\text{Th}_A(\mathcal{M})$, either $\exists \overline{v} \psi(\overline{v})$ or its negation are in $\text{Th}_A(\mathcal{M})$. 
Must $\exists \overline{v} \psi(\overline{v})$ be in $\text{Th}_A(\overline{v})$?
 A: Trust your intuition! But here is a proof if you don't: suppose there is no $\vec{m}$ in $\mathcal{M}$ realising $\psi (\vec{v})$. Then the same is true in every elementary extension of $\mathcal{M}_A$. In particular, $\{ \psi (\vec{v}) \} \cup \textrm{Th} (\mathcal{M}_A)$ is not satisfiable. (Equivalently, one may assert that every $n$-type in the first sense is realised in an elementary extension of $\mathcal{M}_A$, by Gödel's completeness theorem.)
A: Suppose $p\cup \text{Th}_A(\mathcal{M})$ is satisfiable and let $\Delta$ be finite subset of $p$ and $\psi(\bar{v})$ be the conjunction of all formulas in $\Delta$. Since $\text{Th}_A(\mathcal{M})$ is complete in $\mathcal{L}_A$  either $\exists \bar{v} \psi(\bar{v})\in\text{Th}_A(\mathcal{M})$ or $\neg\exists \bar{v} \psi(\bar{v})\in \text{Th}_A(\mathcal{M})$. The later however cannot be (since then $\Delta \cup \text{Th}_A(\mathcal{M})$ would not be satisfiable). So $\Delta$ is realized in $\mathcal{M}$ as stated by Definition 2. 
For the other direction if $p\cup\text{Th}_A(\mathcal{M})$ is not satisfiable then by compactness for some finite $\Delta\subset p$ it holds that $\Delta \cup \text{Th}_A(\mathcal{M})$ is not consistent. So models of $\text{Th}_A(\mathcal{M})$ do not realize $\Delta$, namely (denoting $\psi(\bar{v})$ the conjunction of formulas in $\Delta$) we have $\neg\exists \bar{v} \psi(\bar{v})\in \text{Th}_A(\mathcal{M})$, and in particular $\Delta$ is not realized in $\mathcal{M}$.
