Zero-knowledge proof of $\beta\eta$ equality
I doubt that a zero-knowledge proof is possible, because it seems likely that any finite proof will leak at least partial information about the length of the path that converts $t_1$ to $t_2$, and hence won't be zero-knowledge.  In particular, suppose Alice and Bob's interaction takes $T$ time steps.  Then in any reasonable proof I can imagine, Bob would be able to infer that $t_1$ can be converted to $t_2$ using a path of length at most $T$.  This is partial knowledge, because there exists a pair $t_1,t_2$ of terms that take strictly more than $T$ time steps to convert.

I suspect that we might need an additional condition, such that there is a fixed and known upper bound $B$ on the length of the path converting $t_1$ to $t_2$.  If you have such a bound, there is a zero-knowledge proof protocol whose complexity is polynomial in $B$, as the statement you are proving becomes a NP-statement, and it is known that there are zero-knowledge protocols for every language in NP.