次の例を検討してください。
Theorem example: forall (P: nat->Prop), P (1+2+3) -> (exists x, P x).
Proof.
intros.
apply H
apply H失敗します
Unable to unify "P (1 + 2 + 3)" with "exists x : nat, P x".
したがって、ここで適用するために戦術を使用できることを知っています。または、この他のスタックオーバーフローの質問exists 1+2+3に基づいて、前方推論を使用してそれを実存的な形にするためのより複雑な方法があります。H
しかし、明示的でなくても、統一時に存在変数をインスタンス化できるスマートな戦術があると思いますか?