(FIX  q  L  x  (TC 1)
      (              (  ( (L x) @ 1 ) & ( (L = a) ! (L = b) ) )
                                      ! 
         (E atr y q  (  ( (L x) @ y ) & ( (L = a) ! (L = b) ) ) )
      )
)