diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 3bb3fbff7f593c2c84c3e27d67a9675132aa6aa1..2bbb8c165edde15c0e3450c9763cfcc00b9ab0b4 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -119,7 +119,8 @@ Section heap.
     P ⊑ wp E (Alloc e) Q.
   Proof.
     intros HN ? ? HP. eapply wp_alloc_heap with (σ:=∅); try eassumption.
-    rewrite HP. rewrite left_id.
+    rewrite HP. Fail rewrite left_id.
+  Abort.
 
   Lemma wp_load_heap N E γ σ l v P Q :
     σ !! l = Some v →