Problemi di replica della prova del teorema del punto fisso del calcolo Lambda

Question

Da pag. 35 di Calcolo e combinatori Lambda Un'introduzione:

Corollario 3.3.1 In $ lambda $ e $ cl $: per ogni $ z $ e $ n ge 0 $, l'equazione

$$ xy_1 ldots y_n = z $$

può essere risolto per $ x $. Cioè, c'è un termine $ x $ tale che

$$ xy_1 ldots y_n = _ { beta, w} [x/x] z. $$

Prova: Scegli $ x equiv mathsf {y} ( lambda x y_1 ldots y_n.z) $.

Nota: nel libro, supponiamo che $ mathsf {y} equiv ( lambda ux. Xuux) ( lambda ux. Xuux) $. Inoltre, per facilità di notazione, lascia $ v equiv ( lambda x y_1 ldots y_n.z) $.

Il problema è che quando lo controllo con i miei esempi, non ottengo questo risultato.

Ad esempio, supponiamo che né $ x $ né nessuno di $ y_1, ldots, y_n $ sia nelle variabili gratuite di $ z $ (per renderlo facile). Quindi questo teorema afferma che se $ x equiv mathsf {y} ( lambda x y_1 ldots y_n. Z) $, quindi

$$ xy_1 ldots y_n = _ { beta, w} z $$

Quando controllo se questo è vero, ottengo

$$ ( mathsf {y} ( lambda x y_1 ldots y_n. z)) y_1 ldots y_n = ( mathsf {y} v) y_1 ldots y_n = (v mathsf {y} v) y_1 ldots y_n = _ { beta, w} zy_n $$

Sto facendo qualcosa di sbagliato?