なるほどレスどうも。
ところで、型付でないラムダ計算の世界にも
カリー・ハワードの対応は存在しますか？