diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index f899393a306d89eda35e76fe902b57a1a03c2fad..af482f59e08f483248faeec14181824246130d6a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -426,13 +426,14 @@ Tactic Notation "iApply" open_constr(lem) :=
| ITrm ?t ?xs ?pat => constr:(ITrm t xs ("*" +:+ pat))
| _ => constr:(ITrm lem hnil "*")
end in
- iPoseProofCore lem as false true (fun H => first
- [iExact H
- |eapply tac_apply with _ H _ _ _;
+ let rec go H := first
+ [eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity
- |let P := match goal with |- IntoWand ?P _ _ => P end in
- apply _ || fail 1 "iApply: cannot apply" P
- |lazy beta (* reduce betas created by instantiation *)]]).
+ |apply _
+ |lazy beta (* reduce betas created by instantiation *)]
+ |iSpecializePat H "[-]"; last go H] in
+ iPoseProofCore lem as false true (fun H =>
+ first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 147edd8e6b6572b91d061697bfe4dd9de6bac8e3..f8302508d70aec9fefcb30f7045fc9e7e0ecd195 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -116,3 +116,7 @@ Proof.
iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". }
done.
Qed.
+
+Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
+ (P -∗ Q -∗ True -∗ True -∗ R) -∗ P -∗ Q -∗ R.
+Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.