在 Coq 中执行通用实例化的最佳方式

Question

假设我有一个假设和上下文中的H : forall ( x : X ), P x变量。x : X我想进行通用实例化并获得新的假设H' : P x。最无痛的方法是什么？显然apply H in x不起作用。assert ( P x )其次是apply Hdos，但是如果很复杂的话可能会变得非常混乱P。

有一个类似的问题似乎有些相关。但不确定它是否可以应用在这里。

Answer 1

pose proof (H x) as H'.

括号是可选的。