Honest definitions and UDTFS I am trying to understand the Chernikov-Simon theorem on Uniform Definability of Types over Finite Sets see Corollary 6.17 in Pierre Simon's book.
The proof rests on two results. One is the so-called (p,q)-theorem, a deep result in combinatorics. The second ingredient is Theorem 3.13 in Pierre Simon's book:

Theorem  (honest definitions). Let $M\models T$, $A\subseteq M$, $\phi(x;y) \in L$ a formula and $b\in M^{|y|}$ a tuple. Then there is an elementary extension $(M,A)\prec (M',A')$, a formula $\psi(x;z)\in L$ and a tuple $d$ of elements of $A'$ such that $$\phi(A;b)\subseteq \psi(A';d) \subseteq \phi(A';b).$$

I am puzzled because the theorem above seems trivial when $A$ is finite. Though this is exactly the case relevant for Corollary 6.17.
 A: You're correct that the statement of Theorem 3.13 is trivial when $A$ is finite. This is just because types over finite sets are trivially definable in any theory: For a finite set $A$ and a formula $\phi(x;y)$, the set $\phi(A;b)$ can be defined by $\psi(A;d)$, using parameters $d$ from $A$, just by taking $\psi$ to be $\bigvee_{i=1}^k (x = d_k)$ when $|\phi(A;b)| = \{d_1,\dots,d_k\}$. 
Of course, the key issue here is uniformity: The formula $\psi$ above depended on the size of $\phi(A;b)$. We'd like to be able to pick a formula $\psi(x;z)$ which only depends on $\phi(x;y)$, which works for every finite set $A$ and every tuple of parameters $b$. 
And note how Theorem 3.13 gets used in the proof. It's in the middle of a (technical) uniformity result, Lemma 6.16 of A Guide to NIP Theories. Roughly speaking, if we want to achieve uniformity over arbitrary finite sets, compactness implies that we're going to have to "handle" infinite sets too: We introduce a new unary predicate $P$ which names the set $A$, and we can't axiomatize "$P$ is finite". But the honest definitions theorem is strong enough to give us the right kind of leverage on infinite sets in this compactness argument. 
