We consider the system 478.

  Alphabet:

    a : [] --> o 
    f : [o -> o] --> o 
    g : [o] --> o 
    h : [o] --> o 
    i : [o] --> o 

  Rules:

    f(/\x.X(x)) => X(a) 
    g(a) => f(/\x.i(x)) 
    i(X) => h(g(X)) 

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

  g(a) 
    => f(/\x.i(x)) 
    => f(/\x.h(g(x))) 
    => h(g(a)) 
    |> g(a) 

That is, a term s reduces to a term t which has a subterm that is an instance of the original term.