2016-02-12から1日間の記事一覧
存在証明が絡むとややこしくなったのでメモ (** **** Exercise: 1 star (dist_not_exists) *) (** Prove that "[P] holds for all [x]" implies "there is no [x] for which [P] does not hold." *) Theorem dist_not_exists : forall (X:Type) (P : X -> Pr…
存在証明が絡むとややこしくなったのでメモ (** **** Exercise: 1 star (dist_not_exists) *) (** Prove that "[P] holds for all [x]" implies "there is no [x] for which [P] does not hold." *) Theorem dist_not_exists : forall (X:Type) (P : X -> Pr…