型で、なんかコンパイラに証明させようかと思ったんですよ。