We consider the system 772.

  Alphabet:

    forall : [term -> form] --> form 

  Rules:

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

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

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

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