We consider the system 764.

  Alphabet:

    a : [] --> o 
    b : [] --> o 
    c : [] --> o 
    d : [] --> o 
    f : [o -> o -> o] --> o 

  Rules:

    f(/\x./\y.X(x)) => b 
    b => f(/\x./\y.a) 
    b => c 
    f(/\x./\y.a) => d 

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

  b 
    => f(/\x./\y.a) 
    => b 

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