diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ec00c04ab4e70ee0c9ba9d198b65f9ecf7c829bd..331ec21ebaa4d0cd88cd356141c466e3f5b160d7 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -45,9 +45,13 @@ Ltac iMatchGoal tac :=
 Tactic Notation "iProof" :=
   lazymatch goal with
   | |- of_envs _ ⊢ _ => fail "iProof: already in Iris proofmode"
-  | |- True ⊢ _ => apply tac_adequate
-  | |- _ ⊢ _ => apply uPred.wand_entails, tac_adequate
-  | |- _ ⊣⊢ _ => apply uPred.iff_equiv, tac_adequate
+  | |- ?P =>
+    match eval hnf in P with
+    | True ⊢ _ => apply tac_adequate
+    | _ ⊢ _ => apply uPred.wand_entails, tac_adequate
+    (* need to use the unfolded version of [⊣⊢] due to the hnf *)
+    | uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
+    end
   end.
 
 (** * Context manipulation *)