Search code examples
coqcoq-tactic

coq: elimination of forall quantifier

I want to prove the following theorem:

Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
  (q \/ forall x : A, p x) -> (forall x : A, q \/ p x).

I already got the following piece of the proof:

Proof.
intro.
intro.
destruct H.
left.
assumption.

But now I am in a situation I don't know what to do. The following things are at my disposal:

A : Set
q : Prop
p : A -> Prop
H : forall x : A, p x
x : A

And I would like to prove the following subgoal:

q \/ p x

How can I eliminate the forall quantifier in the given premise

forall x : A, p x

that is: How can I plug in my concrete x : A so that I can deduce: p x ?

Solution

  • You can instantiate the universally quantified x in H with specialize (specialize (H x)).