u = (_t1::forall s a. ST s (forall s'. ST s' a))