diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index b4eadc21f6149b63921680869556b9cf89964d0f..8a1dd28eddb232a0a1bdbccfb9bd6ec84e8c6f06 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -140,13 +140,13 @@ Section heap.
   Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
 
   (** Weakest precondition *)
-  Lemma wp_alloc N E e v P Φ :
+  Lemma wp_alloc N E e v Φ :
     to_val e = Some v → nclose N ⊆ E →
     (heap_ctx N ★ ▷ ∀ l, l ↦ v -★ Φ (LitV $ LitLoc l)) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    (* TODO: use an iTactic *)
+    (* TODO: change [auth_fsa] to single turnstile and use [iApply] *)
     apply (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
     iFrame "Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
@@ -156,10 +156,8 @@ Section heap.
     rewrite [{[ _ := _ ]} ⋅ ∅]right_id.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
     iFrame "Hheap". iSplit.
-    { (* FIXME iTactic for introduction of constant assertions? *)
-      rewrite const_equiv; first done. split; first done.
-      by apply (insert_valid h). }
-    iIntros "Hheap". iApply "HΦ". rewrite /heap_mapsto. done.
+    { iPureIntro; split; first done. by apply (insert_valid h). }
+    iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
   Qed.
 
   Lemma wp_load N E l q v P Φ :
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index e0c6d31fc82cc6ae36851cd6696c324f4507a14f..737450a97c1c969490bc7979390e8e1dc1c6fbcb 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -25,8 +25,8 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
     Δ'' ⊢ Φ (LitV (LitLoc l))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. etrans; last apply: wp_alloc; eauto.
-  rewrite -always_and_sep_l. iSplit; first done.
+  intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
+  apply and_intro; first done.
   rewrite strip_later_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.