Unique increasing function solution $y(x)$ such that $f_0(x) = f_1(y(x))$

Question

I have the function $y(x)$ defined as the solution to following equation:

$f_0(x) = f_1(y(x)) \quad \forall x \in [0,1]$.

With $f_0, f_1$ known, continuous, continuously différentiable and bounded between [-1,1]. And I know that $y(x): [0,1] \rightarrow [0,1]$ is strictly increasing with $y(0) = 0$ and $y(1)=1$.

I know there exists a strictly increasing solution $y(x)$ going from 0 to 1. I need to prove that this solution is unique.
Remark: if $f_0$ is monotone, then I can just invert it and the solution is direct, but here I’m in a more general case.

The solution should be unique as long as $f_j$ are never flat (i.e. the set of points such that $df_j/dx = 0$ is of null measure. Or maybe I can phrase it differently?).
My intuition is really simple: it follows from a graph analysis; The two curves should pass by exactly the same point, in the same order (just not with the same ‘speed’)
i.e. the first $x$ such that $f_0(x) = k$ corresponds to the first $y$ such that $f_1(y) = k$ and so on.
So, as long as I have no flat part, it is impossible for me to find several match to a given point.

I find the idea trivial, however I struggle to write down a proof for this. I have 3 ways, none really satisfying (though often close...)

1. I first tried to write a proof where I do piecewise inversion of the functions between every points where $df_j/dx = 0$ (because between these points, the function is monotonous). However apparently it’s not correct to talk about the points where this is true (because there might exist some very particular functions such that this set of point is infinite for example, for which this proof might be more clumpsy).

2. Now I’m trying to write a proof by absurdity: trying to show that the only way to end up with two solutions is to have some flatness. But I still end up at some point on “counting how much point there is with $df_j/dx = 0$”. Which I would like to avoid at all cost.

3. Finally I think I can find a solution using nonlinear differential equations properties. Using Picard-Lindelof theorem. However, my equation will not be defined at the points where $df_j/dx = 0$, so I’m not sure I can apply Picard-Lindelof directly here (in the idea, the proof still work, I go from x=0 to the first x where $df_0/dx=0$ on the solution path. Then I start again right after this $x$ up to the next point where $df_0/dx=0$, and so on, and so forth.
   I’m not sure there exists a variant of Picard-Lindelof for this case (i.e. allowing for undefined point wise 0/0 on the optimal path). But anyway, I’m more interested in a proof using one of the other two methods (might be more intuitive).