diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 18c37ea8b6ac1d2ac13d16ee41b9d4be4f691299..663ec941274d6888054be0b631df0ff3fc244c1c 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -18,7 +18,7 @@ Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
 Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. intros ?%subG_inG. split; apply _. Qed.
 
 Section proof.
   Context `{!heapG Σ, !lockG Σ} (N : namespace).