coqproofpredicates

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)?

Solution

  • The answer is:

    specialize H with c.