Hello,

I have just started using coq and couldn’t find a solution to this Problem.

#### Question

How can I use the `apply .. in`

tactic, when the desired conclusion begins with ∀?

#### (Toy) Example:

I am trying to prove the following theorem:

```
Theorem noworks : forall (X : Type) (P : X -> Prop) (A : Prop) (x' : X),
A -> (A -> (forall x, P x)) -> P x'.
```

This proof attempt where I try using the premises to arrive at ∀x P x fails.

```
Proof.
intros X P A x HA Himp. apply Himp in HA.
> Output: Unable to find an instance for the variable x.
```

If however I replace the ∀x P x in the theorem by a helper definition, the Proof works the intended way.

```
Definition helper (X : Type) (P : X -> Prop) : Prop :=
forall x, P x.
Theorem works : forall (X : Type) (P : X -> Prop) (A : Prop) (x' : X),
A -> (A -> helper X P) -> P x'.
(* ^^^^^^^^^^ *)
Proof.
intros X P A x HA Himp. apply Himp in HA. unfold helper in HA. apply HA.
Qed.
```

I’d also appreciate any tips on how to troubleshoot these kinds of issues (e.g. using the documentation).

Thanks for your help!