forall についての雑文 さて、ここで教科書の Coq in a Hurry に戻ると、私が作った「風が吹く」「桶屋が儲かる」なんかの命題を Variable で定義する代わりに、forall というキーワードを使っています。つまり、 Variable 風が吹く 桶屋が儲かる : Prop. Th…