>>232
> このラムダ式が定義できる事が、証明した事になるのかな?
疑問点がいまいちわかんない。
直観主義命題論理の証明と Lisp の関数とが対応するかということなら、
少なくとも上に書いたような方法では対応させられないと思う。