diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 69a018f5c095634b77e232a7761e6fb617c187f9..91987e6fc6b10cd397d734ce1954161451d65697 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -86,12 +86,14 @@ Section heap.
       apply to_heap_valid. }
     apply pvs_mono, exist_elim=> γ.
     rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
+    rewrite /heap_mapsto_def /heap_name.
     induction σ as [|l v σ Hl IH] using map_ind.
     { rewrite big_sepM_empty; apply True_intro. }
     rewrite to_heap_insert big_sepM_insert //.
     rewrite (map_insert_singleton_op (to_heap σ));
       last rewrite lookup_fmap Hl; auto.
-    by rewrite auth_own_op IH.
+    (* FIXME: investigate why we have to unfold auth_own here. *)
+    by rewrite auth_own_op IH auth_own_eq. 
   Qed.
 
   Context `{heapG Σ}.