( (U x)  atr  x  1
            (  ( ( atr x) @ 1 ) &                 
               (E  l y x   ( (l = a) ! (l = b) ) )
            )
)