We consider the system 775.

  Alphabet:

    letval : [expr * val -> expr] --> expr 

  Rules:

    letval(X, /\x.letval(Y, /\y.Z(x, y))) => letval(Y, /\z.letval(X, /\u.Z(u, z))) 

It is easy to see that this system is non-terminating:

  letval(x, /\y.letval(z, /\u.f y u)) 
    => letval(z, /\y.letval(x, /\u.f u y)) 
    => letval(x, /\y.letval(z, /\u.f y u)) 

That is, a term s reduces to a term t which instantiates s.