2015-01-09 命題と証明 in coq そういや、: の左は、値。右は型。だった。 あるいは、: の左は証明。右は命題。 あるいは、: の左は命題。 右は命題型。つまり、 なんらかの命題 : Prop右に命題を書いてしまえば、左はその証明を用意しなくちゃならない。