"iApply ... with" unifies with assumptions before taking goal into account
The following test case fails:
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
This is fairly annoying when working with higher-order lemmas, for example it came up in the logically atomic context when trying to apply
Lemma astep_intro Eo Em α P β Φ x :
α x -∗
((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗
atomic_step Eo Em α P β Φ.
where α : A -> PROP
. Now iApply (astep_intro with "foo")
fails to apply in most cases because it infers the wrong α
.