We consider the system 781.

  Alphabet:

    choice : [A * A] --> A 
    new : [N -> A] --> A 

  Rules:

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

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

  choice(x, y) 
    => choice(y, x) 

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