>>230
(lambda (x) (funcall (cdr x) (car x)))

:t ¥x -> (snd x) (fst x)
に対応しているのは分かるんだけれど、
このラムダ式が定義できる事が、証明した事になるのかな?