# Using \`apply .. in\` when conclusion contains forall

**URL:** <https://discourse.rocq-prover.org/t/using-apply-in-when-conclusion-contains-forall/649>\
**Category:** Using Rocq\
**Created:** [February 27, 2020, 8:22pm UTC](https://discourse.rocq-prover.org/t/using-apply-in-when-conclusion-contains-forall/649 "2020-02-27T20:22:12Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![mguerdi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mguerdi/32/378_2.png) [@mguerdi](https://discourse.rocq-prover.org/u/mguerdi)\
**Post date:** [February 27, 2020, 8:22pm UTC](https://discourse.rocq-prover.org/t/using-apply-in-when-conclusion-contains-forall/649/1 "2020-02-27T20:22:12Z")

</div>

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:

```auto
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.

```auto
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.

```auto
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!

---

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [February 28, 2020, 2:01pm UTC](https://discourse.rocq-prover.org/t/using-apply-in-when-conclusion-contains-forall/649/2 "2020-02-28T14:01:44Z")

</div>

Hello,

It’s a bit of a quirky behavior of the `apply` tactic. When you apply `Himp`, it tries to give you a goal containing what is interpreted as the conclusion of the hypothesis. To do so, it considers that anything to the left of an arrow is an hypothesis that should be discharged, and anything quantified should be instantiated.  
So as long as it’s “hypotheses”, it just gives you new goals. I.e. if you had instead:

> Theorem noworks : forall (X : Type) (P : X → Prop) (A : Prop) (x’ : X),  
> A → (A → (A → P x’)) → P x’.

Then `apply Himp in HA` would work and generate a second goal, asking for a proof of `A`.  
However when it comes to quantifiers, `apply` does not generate goals for them, hence the failure. You can instead use `eapply` (where the `e` stands for existential) to introduce `evars` when it finds quantifiers that it cannot instantiate. I.e. coming back to your initial example, `eapply Himp in HA` works and gives you an hypothesis of the form `HA: P ?x` that you can use to conclude your goal since Coq will then happily unify `?x` with `x`.

Finally you sometimes want to keep the quantifier in your hypothesis, in particular because you might want to use it for two different values of `X`. One simple way to do so here is to use `specialize` instead of `apply`: `specialize (Himp HA)` will do what you want.

Hope it helps,  
Yannick