We consider the system 782.

  Alphabet:

    nu : [I -> I] --> I 

  Rules:

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

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

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

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