# `iApply` does not use `FromAssumption` for goal matching

```
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
(P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
```

When using `iApply`

in combination with the `with`

clause, it will first `iSpecialize`

and then use `iApply`

, which in these examples turns to the degenerate case of `iExact`

. The `iExact`

tactic uses `FromAssumption`

to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).

When using `iApply`

without the `with`

clause, it will launch a search using `IntoWand`

where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.

The problem is the instance:

```
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```

Here, `Q`

should match exactly. I tried strengtening it to:

```
Global Instance into_wand_wand p q P Q P' Q' :
FromAssumption q P P' →
FromAssumption (p && q) Q' Q →
IntoWand p q (P' -∗ Q') P Q.
```

However, that causes other problems: in some cases the above instance will be triggered instead of instances like `into_wand_bupd_args`

causing the following to go wrong:

```
Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
(P -∗ Q) -∗ |==> Q.
Proof.
iIntros "H".
iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)
```

This issue came up in practice Simuliris.