Coq が存在量化を扱う途中で混乱しています。
述語 P と仮定 H があります
P : nat -> Prop
H : exists n, P n
現在の目標は（何でも）
(Some goal)
H で n をインスタンス化したい場合は、そうします
elim H.
ただし、削除後、現在の目標は
forall n, P n -> (Some goal)
Coq が存在量指定子を普遍的な量指定子に変換しているようです。(forall a, P a -> Q a) -> ((exists a, P a) -> Q a)ということは、一階論理に関する限られた知識から知っています。しかし、逆の命題は正しくないようです。「forall」と「exists」が同等でない場合、なぜ Coq はそのような変換を行うのでしょうか?
Coqの「elim」は、目標を証明するのが難しいものに置き換えますか? または、((exists a, P a) -> Q a) -> (forall a, P a -> Q a)が一階論理で成立する理由を誰かが示してくれませんか?