Consideriamo il termine
             _             _
  new y in ( xy | R) | (xw.wa)

ovviamente dovremmo essere capaci di derivare, nell'LTS,
il giudizio 
                   
                    _             _                            _
A,x,a|-  new y in ( xy | R) | (xw.wa) --tau-->  new y in ( R | ya)

Con la nuova regola, quello che potremmo derivare e' pero'

                                 _                            _
A,x,a|- new y in ( xy | R) | (xw.wa) --tau-->  (new y in R) | ya

che ha per' tutto un altro senso, poiche' non si fa vedere
che il nome y e' privato anche per    _ 
                                      ya


Esercizio: dimostrare formalmente, usando le regole dell'LTS normale,
che 

                    _             _                            _
A,x,a|-  new y in ( xy | R) | (xw.wa) --tau-->  new y in ( R | ya)