diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 67d73d853d1572e8d998ac93aa7bcad1de6768f4..075101768b3dbb663d007719f4058bdd48fc251c 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -11,7 +11,8 @@ Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Hint Resolve head_prim_reducible head_reducible_prim_step : core.
-Hint Resolve (reducible_not_val _ inhabitant) : core.
+Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
+Hint Resolve reducible_not_val_inhabitant : core.
 Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 85109f320b5c57a53af92b9aab6edd89dadc0541..72e75d5cdbd22df474cfac8a1bb729f26bb7595f 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -209,7 +209,8 @@ Section ectx_lifting.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types e : expr Λ.
   Hint Resolve head_prim_reducible head_reducible_prim_step : core.
-  Hint Resolve (reducible_not_val _ inhabitant) : core.
+  Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
+  Hint Resolve reducible_not_val_inhabitant : core.
   Hint Resolve head_stuck_stuck : core.
 
   Lemma ownP_lift_head_step s E Φ e1 :