coq - 将假设应用于变量

Question

假设我正在做一个证明，并且我有这样的假设：

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

和 somePred 的定义说：

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

我如何申请H和c获得P(c, a, b)？

score 1 · Accepted Answer

1

答案是：

specialize H with c.

于 2015-03-28T14:37:16.993 回答

1 回答 1