((λy.xy)(λz.y(λy.x)))[xyz/x]

rinominiamo le variabili legate del termine ((λy.xy)(λz.y(λy.x))) per poter effettuare la sostituzione (evitando cosi' che una delle variabili libere del termine (xyz) finisca nel campo di azione (scope) di un lambda che lega una variabile con lo stesso nome)
((λa.xa)(λb.y(λc.x)))[xyz/x]

possiamo ora sostituire il termine (xyz) al posto della variabile libera x.

((λa.(xyz)a)(λb.y(λc.(xyz))))