We consider the system 774.

  Alphabet:

    0 : [] --> G 
    app : [ArGG * G] --> G 
    lam : [G -> G] --> ArGG 
    union : [G * G] --> G 

  Rules:

    app(lam(/\x.X(x)), Y) => X(Y) 
    lam(/\x.app(X, x)) => X 
    union(X, 0) => X 
    union(0, X) => X 
    union(union(X, Y), Z) => union(X, union(Y, Z)) 
    union(X, Y) => union(Y, X) 

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

  union(x, 0) 
    => union(0, x) 
    => union(x, 0) 

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