動的型付けの証明支援系ってのは何をしてるんだ?