You have already assigned T4
to z(z(y x))
, so we can use it in the last equation.
T3 = T5 -> T6 //z(y x)
T3 = T6 -> T4 //z(z(y x))
Since T5 -> T6 = T6 -> T4
, it follows that T5 = T6
and T6 = T4
.