coq - Coqでユニバーサルインスタンス化を実行する最良の方法

Question

コンテキストに仮説H : forall ( x : X ), P xと変数x : Xがあるとします。普遍的なインスタンス化を実行して、新しい仮説を取得したいH' : P x。これを行うための最も痛みのない方法は何ですか? どうやらapply H in x機能しません。assert ( P x )do が続きますが、複雑apply Hな場合は非常に面倒になる可能性があります。P

多少関連していると思われる同様の質問があります。ただし、ここで適用できるかどうかはわかりません。

Answer 1

pose proof (H x) as H'.

括弧はオプションです。

Answer 2

次のようなものを使用できますgeneralize (H x); intros Hx:現在の目標の前に新しい含意としてgeneralize追加され、仮説に入れられます。(H x)intros