We consider the system 783.

  Alphabet:

    r : [i -> o] --> o 

  Rules:

    r(/\x.r(/\y.X(x, y))) => r(/\z.r(/\u.X(u, z))) 

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

  r(/\x.r(/\y.f x y)) 
    => r(/\x.r(/\y.f y x)) 
    => r(/\x.r(/\y.f x y)) 

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