How to prove the theory of algebraically closed valued fields is a NIP theory? Let $T$ be a complete $L$-theory. An $L$-formula $\phi(x,y)$ is said to have the independence property (with respect to $x, y$) if in every model $M$ of $T$ there is, for each $n = \{\,0,1,\dots,n − 1\,\} < \omega$, a family of tuples $b_0,\dots,b_{n−1}$ such that for each of the $2n$ subsets $X$ of $n$ there is a tuple $a$ in $M$ for which $$M\models\varphi(\boldsymbol{a},\boldsymbol{b}_i)\quad\Leftrightarrow\quad  i\in X.$$
The theory $T$ is said to have the independence property if some formula has the independence property. If no $L$-formula has the independence property then $T$ is called dependent, or said to satisfy NIP. An $L$-structure is said to have the independence property (respectively, NIP) if its theory has the independence property (respectively, NIP). [Wikipedia]
Where can I find a proof to show that the theory of algebraically closed valued fields is a NIP theory?
 A: The proof of this has two main components: 


*

*Quantifier elimination for ACVF (in an appropriate language). This allows us to understand all of the definable sets in one free variable. In particular, ACVF has a property called C-minimality, which says that all definable sets in one free variable have a certain form. 

*The fact that NIP can be checked for formulas in one free "object" variable (the $x$ in your definition of the independence property). 


Putting these two components together, we can prove that ACVF is NIP by checking that no formula in one object variable has the independence property, which follows from the classification of such formulas given by quantifier elimination. More abstractly, every C-minimal theory is NIP. 
I suspect the reason why it's tricky to track down a complete reference for this theorem is that components 1 and 2 were both well-known (without the language of C-minimality) before anyone asked the question "is ACVF NIP?". Since that question can be answered fairly easily by putting together the two well-known results, the answer became folklore. Most sources just assert it, giving references to 1 and 2 and leaving the verification as an exercise to the reader. 
One place where there is a complete proof is the paper On variants of o-minimality by Macpherson and Steinhorn, where the notion of C-minimality was first introduced. Proposition 3.4 of that paper says that C-minimal structures are NIP, and Theorem 4.11 says that ACVF is C-minimal (with a reference to another source for the necessary quantifier elimination result).
