In this paper we present strong normalisation proofs using a technique of non-deterministic translations into Klop's extended lambda-calculus. We first illustrate the technique by showing strong normalisation of a typed calculus that corresponds to natural deduction with general elimination rules. Then we study its explicit substitution version, the type-free calculus of which does not satisfy PSN with respect to reduction of the original calculus; nevertheless it is shown that typed terms are strongly normalising with respect to reduction of the explicit substitution calculus. In the same framework we prove strong normalisation of SÃ¸rensen and Urzyczyn's cut-elimination system in intuitionistic sequent calculus.