diff --git a/barrier/lifting.v b/barrier/lifting.v
index 43a1f3c3e9fb4738735d758d99418f1cafa52a93..0e0dd24fc8130381614cb1a04a3aba34d1b5fe70 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -188,11 +188,9 @@ Proof.
   by asimpl.
 Qed.
 
-Lemma wp_plus n1 n2 E P Q :
-  P ⊑ Q (LitNatV (n1 + n2)) →
-  ▷P ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
+Lemma wp_plus n1 n2 E Q :
+  ▷Q (LitNatV (n1 + n2)) ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros HP.
   etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = LitNat (n1 + n2)); last first.
   - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
diff --git a/barrier/tests.v b/barrier/tests.v
index f00b2246173f87802b91b6e73b026243c9a33641..ee8aeeffff233b346bc2b46e87dadb430f846773 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -47,7 +47,7 @@ Module LiftingTests.
     { eapply wp_load. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
     move=>v; apply const_elim_l; move=>-> {v}.
     rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
-    rewrite (later_intro (ownP _)); apply wp_plus.
+    rewrite -wp_plus -later_intro.
     rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
     rewrite -wp_mono.
     { eapply wp_store; first reflexivity. apply: lookup_insert. }