You can trace through what happens then if we apply \[[who(i)]] to (\[[spurned]] applied to \[[Alice]] and \[[i]]):
- [[Alice spurned i]] = [[spurned]] [[Alice]] [[i]]
+ \[[Alice spurned i]] = \[[spurned]] \[[Alice]] \[[i]]
= (lift2 S) (unit Alice) (lookup i)
= bind (unit Alice) (fun x -> bind (lookup i) (fun y -> unit (S x y)))
And now supplying \[[Alice spurned i]] as an argument to \[[who(i)]], we get:
- [[who(i): Alice spurned i]] = [[who(i)]] [[Alice spurned i]]
+ \[[who(i): Alice spurned i]] = \[[who(i)]] \[[Alice spurned i]]
= (fun u v -> shift i v u) (fun e -> S Alice (lookup i e))
= fun v -> shift i v (fun e -> S Alice (lookup i e))