ものまね鳥をまねる coqで
Pである鳥 Aがいて、Qである鳥 Bがいる場合 Xである鳥がいることを示せ。みたいな問題で、
(exists A, P A) -> (exists B, Q B) -> exists C, X C.
のように立式してたけど、
forall A B, P A -> Q B -> exists C, X C.
でいいのか?
証明も少し楽だ。 destructせんでええし。
Pである鳥 Aがいて、Qである鳥 Bがいる場合 Xである鳥がいることを示せ。みたいな問題で、
(exists A, P A) -> (exists B, Q B) -> exists C, X C.
のように立式してたけど、
forall A B, P A -> Q B -> exists C, X C.
でいいのか?
証明も少し楽だ。 destructせんでええし。