diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index ae9d3dadee3485f03a88d02ad1ba01b26ce02a28..e51974e0260253e43b896516f27d21a55571d937 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -17,8 +17,9 @@ Class heapGS Σ := HeapGS {
   heapGS_inv_heapGS :> inv_heapGS loc (option val) Σ;
   heapGS_proph_mapGS :> proph_mapGS proph_id (val * val) Σ;
   heapGS_step_name : gname;
-  heapGS_step_cnt :> mono_natG Σ;
+  heapGS_step_cnt : mono_natG Σ;
 }.
+Local Existing Instance heapGS_step_cnt.
 
 Section steps.
   Context `{!heapGS Σ}.