diff --git a/iris_meta.v b/iris_meta.v
index 7bb4d79d78d3914f70baa2d8bf42da1078bd8194..effbc85828a4502591f5217bc3c16fbc4324ccbc 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -362,7 +362,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
     Qed.
 
     Program Definition plugExpr safe m φ P Q: expr -n> Props :=
-      n[(fun e => (lift_ePred φ e) ∨ (ht safe m P e Q))].
+      n[(fun e' => (lift_ePred φ e') → (ht safe m P e' Q))].
     Next Obligation.
       intros e1 e2 Heq w n' r HLt.
       destruct n as [|n]; [now inversion HLt | simpl in *].