A friend of mine working on Auction Theory needs to establish uniqueness of solution (up to initial and boundary conditions) of a system of differential equations of the form
$$ F(y_1,y_2,y_3,\dot{y}_1,\dot{y}_2,\dot{y_3},x) = 0 \\ y_1(y_2) = y_3 $$
where $F:\mathbb{R}^6\times X\to\mathbb{R}^n$ is a polynomial, $X\subseteq\mathbb{R}$ is a compact set, and $y_1,y_2,y_3:X\to X$ are the functions of interest.
What throws us off is the equation $y_1(y_2) = y_3$. We don't know how to deal with it.
Are there any standard tools that may help him ot establish uniqueness for this sort of problems?