おいおい、プログラム=証明を書いておきながら、型=命題が
わかっていないってことは、プログラマとしてアボーンだよ。
型推論なんかあってもなくても本質的な違いはない。それよりは、
静的型チェックがあることが重要