对变量应用低收缩

Question

假设我正在进行一个证明，我有这样的假设：

a : nat
b : nat
c : nat
H : somePred a b

一些Pred的定义是：

Definition somePred (p:nat) (q:nat) : Prop := forall (x : nat), P(x, p, q).

如何将H应用于c并获得P(c, a, b)？

Answer 1

答案是：

specialize H with c.