es68

Se P -->beta Q allora esiste un sottotermine di P della forma (\x.M)N che viene contratto a M[N/x]. 
Per dimostrare che FV(Q) e' un sottoinsieme di FV(P) basta dimostrare quindi che FV(M[N/x]) e' un sottinsieme di FV((\x.M)N).
Distinguiamo due casi: 
-- x appartiene a FV(M) 
In questo caso in FV(M[N/x]) ci sono tutte le variabili libere di M 
(la x a cui sostituiamo N e' legata in P) piu' tutte le variabili libere di N 
(poiche' per definizione di sostituzione nessuna variabile libera di N diventera' legata dopo la sostituzione. 
Quindi abbiamo che FV(M[N/x]) e' un sottinsieme (in particolare e' uguale a) FV((\x.M)N) 

-- x non appartiene a FV(M) In questo caso, per definizione di sostituzione, FV(M[N/x]) = FV(M). 
Siccome FV((\x.M)N) = FV(\x.M) unito FV(N) abbiamo che FV(M[N/x]) e' un sottinsieme di FV((\x.M)N) 
(in particolare e' uguale se FV(N) = empty. 

La dimostrazione data si potrebbe formalizzare meglio, ma per il livello del nostro corso puo' andare.