diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 5d1b848220050b2de0519937d27d630b773275b9..b356f550a02a286628da3b12dbac3a0046fa77c6 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -74,6 +74,13 @@ Class atomic_heap := AtomicHeap {
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
 
+Global Arguments alloc : simpl never.
+Global Arguments free : simpl never.
+Global Arguments load : simpl never.
+Global Arguments store : simpl never.
+Global Arguments cmpxchg : simpl never.
+Global Arguments mapsto : simpl never.
+
 Existing Class atomic_heapGS.
 Global Hint Mode atomic_heapGS + + : typeclass_instances.
 Global Hint Extern 0 (atomic_heapGS _) => progress simpl : typeclass_instances.
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index a7ba1b21384f940968dce1751eccfa4418b7ec7f..b06b4f1cbe3f40bad6e92b8a84aac74f30061949 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -49,6 +49,12 @@ Class lock := Lock {
     {{{ is_lock (L:=L) γ lk R ∗ locked (L:=L) γ ∗ R }}} release lk {{{ RET #(); True }}}
 }.
 
+Global Arguments newlock : simpl never.
+Global Arguments acquire : simpl never.
+Global Arguments release : simpl never.
+Global Arguments is_lock : simpl never.
+Global Arguments locked : simpl never.
+
 Existing Class lockG.
 Global Hint Mode lockG + + : typeclass_instances.
 Global Hint Extern 0 (lockG _) => progress simpl : typeclass_instances.
diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index d42ed7c52d72c55f8bf450f6852e69d31c324f67..57060fd9814e4bde566e6519d7c2c0a4c3c0c8ec 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -72,6 +72,15 @@ Class rwlock := RwLock {
     {{{ RET #(); True }}};
 }.
 
+Global Arguments newlock : simpl never.
+Global Arguments acquire_reader : simpl never.
+Global Arguments release_reader : simpl never.
+Global Arguments acquire_writer : simpl never.
+Global Arguments release_writer : simpl never.
+Global Arguments is_rw_lock : simpl never.
+Global Arguments reader_locked : simpl never.
+Global Arguments writer_locked : simpl never.
+
 Existing Class rwlockG.
 Global Hint Mode rwlockG + + : typeclass_instances.
 Global Hint Extern 0 (rwlockG _) => progress simpl : typeclass_instances.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 613d78114412de1c14359c7d228eb37c33171eed..114ce325ec24db5c5b02efefc322c559cc7e6778 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -304,3 +304,18 @@ goal 2 is:
 The command has indeed failed with message:
 Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in 
 (#() #()).
+"wp_spin_lock_client"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  spin_lockG0 : spin_lockG Σ
+  loc : locations.loc
+  lock : val
+  γ : lock_name
+  ============================
+  "Hislock" : is_lock γ lock (∃ v : val, loc ↦ v)
+  --------------------------------------â–¡
+  WP let: "lock" := lock in acquire "lock";; #loc <- #42;; release "lock"
+  {{ _, True }}
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index c5f966bb02e09ec68c1dad0510804e8aca7e01ad..eb741db312fa4ba9102c7428032d5be3ffe76e6c 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -550,12 +550,13 @@ Section spin_lock.
   (* Making sure that using [spin_lockG] here works, not just [lockG]. *)
   Context `{!heapGS Σ, !spin_lockG Σ}.
 
+  Check "wp_spin_lock_client".
   Lemma wp_spin_lock_client loc lock γ :
     is_lock γ lock (∃ v, loc ↦ v) -∗
     WP spin_lock_client #loc lock {{ _, True }}.
   Proof.
-    iIntros "#Hislock".
-    wp_lam. wp_smart_apply (acquire_spec with "Hislock") as "[Hlocked [%v Hloc]]".
+    iIntros "#Hislock". wp_lam. simpl. Show.
+    wp_smart_apply (acquire_spec with "Hislock") as "[Hlocked [%v Hloc]]".
     wp_store.
     wp_smart_apply (release_spec with "[$Hlocked Hloc]").
     { iFrame "Hislock". eauto. }