Hola,
El xs que aparece dentro del case no ocurre libre, está ligado por el patrón (x:xs). En otras palabras, el xs de e no es el mismo xs que vamos a sacar con la eta-reducción.
Noten que es lo mismo escribir:
\xs -> (\ys -> case ys of
[] -> 0;
(x : xs) -> 1 + xs) xs
que:
\xs -> (\ys -> case ys of
[] -> 0;
(x : zs) -> 1 + zs) xs
saludos
El xs que aparece dentro del case no ocurre libre, está ligado por el patrón (x:xs). En otras palabras, el xs de e no es el mismo xs que vamos a sacar con la eta-reducción.
Noten que es lo mismo escribir:
\xs -> (\ys -> case ys of
[] -> 0;
(x : xs) -> 1 + xs) xs
que:
\xs -> (\ys -> case ys of
[] -> 0;
(x : zs) -> 1 + zs) xs
saludos