It is Undecidable if Two Regular Tree Languages can be Separated by a Deterministic Tree-walking Automaton

The following problem is shown undecidable: given regular languages L, K of finite trees, decide if there exists a deterministic tree-walking automaton which accepts all trees in L and rejects all trees in K. The proof uses a technique of Kopczyński from [1].