diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4a1451dc32ef2cd1bc08fad3040e931bcfa3f713..ab862cc2bfa10e90a563b4656fe8dad9637d0cf4 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -628,8 +628,8 @@ Tactic Notation "iIntoValid" open_constr(t) :=
       let e := fresh in evar (e:id T);
       let e' := eval unfold e in e in clear e; go (t e')
     | _ =>
-      let tT' := eval cbv zeta in tT in apply (as_valid_1 tT');
-        [apply _ || fail "iPoseProof: not a BI assertion"|exact t]
+      let tT' := eval cbv zeta in tT in eapply (as_valid_1 tT');
+        [solve [ typeclasses eauto with typeclass_instances ] || fail "iPoseProof: not a BI assertion"|exact t]
     end in
   go t.