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