poe123
poe123

Reputation: 1208

Applying hypotesis to a variable

Let's say I'm in the middle of a proof and I have hypotheses like these:

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

and the definition of somePred says:

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

How do I apply H to c and to get P(c, a, b)?

Upvotes: 1

Views: 54

Answers (1)

poe123
poe123

Reputation: 1208

The answer is:

specialize H with c.

Upvotes: 1

Related Questions