diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index d3b16716874ddd7b9c5ebb7e874db7e622144ed3..91fd17a56de34eba228c2bec495c94e13ec9a1c1 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -170,18 +170,6 @@ Proof.
   iIntros "_". iPureIntro. rewrite /num_laters_per_step /=. lia.
 Qed.
 
-(** This just re-exports the lifting lemma when one wants to generate a single
-credit during a pure step. *)
-Lemma wp_pure_step_credit s E e1 e2 ϕ Φ :
-  PureExec ϕ 1 e1 e2 →
-  ϕ →
-  ▷ (£ 1 -∗ WP e2 @ s; E {{ Φ }}) -∗
-  WP e1 @ s; E {{ Φ }}.
-Proof.
-  iIntros (Hexec Hphi) "Hwp".
-  iApply wp_pure_step_later; done.
-Qed.
-
 (** Recursive functions: we do not use this lemmas as it is easier to use Löb
 induction directly, but this demonstrates that we can state the expected
 reasoning principle for recursive functions, without any visible â–·. *)
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index f53dd44909c742bc78284575e71ff0c2c232d491..6a8fd1de71f1300e7987a56cc1e45a6a188ae7c3 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -57,16 +57,16 @@ Lemma tac_wp_pure_credit `{!heapGS_gen hlc Σ} Δ Δ' s E j K e1 e2 ϕ Φ :
   PureExec ϕ 1 e1 e2 →
   ϕ →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  (match envs_app false (Esnoc Enil j (£ 1)) Δ' with
-    | Some Δ'' =>
-       envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
-    | None => False
-    end) →
+  match envs_app false (Esnoc Enil j (£ 1)) Δ' with
+  | Some Δ'' =>
+     envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
+  | None => False
+  end →
   envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal=> ??? HΔ.
   pose proof @pure_exec_fill.
-  rewrite -wp_pure_step_credit; last done.
+  rewrite -lifting.wp_pure_step_later; last done.
   rewrite into_laterN_env_sound /=. apply later_mono.
   destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
   rewrite envs_app_sound //; simpl.
@@ -161,7 +161,7 @@ Tactic Notation "wp_pure" open_constr(efoc) "credit:" constr(H) :=
   let Htmp := iFresh in
   let finish _ :=
     pm_reduce;
-    (iDestructHyp Htmp as H || fail 2 "wp_pure: " H " is not fresh");
+    (iDestructHyp Htmp as H || fail 2 "wp_pure:" H "is not fresh");
     wp_finish
     in
   lazymatch goal with
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 3835c2cbeae482d951a6b78556d8866dfd64a463..f85b167b4a75467c954fcb064dcc818cd93f1355 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -193,7 +193,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 "test_wp_pure_credit_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: wp_pure:  "Hcred"  is not fresh.
+Tactic failure: wp_pure: "Hcred" is not fresh.
 1 goal
   
   Σ : gFunctors