diff --git a/barrier/tests.v b/barrier/tests.v
index 32a2d738ad0f033b6dcd8f1425909ff44c9543a2..499f9351b23895892a6c5fad47877d84c9d647e2 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -115,4 +115,11 @@ Module LiftingTests.
       + by apply const_intro; omega.
       + done.
   Qed.
+
+  Goal ∀ E, True ⊑ wp (Σ:=Σ) E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
+  Proof.
+    intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
+    asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
+    rewrite -Pred_spec -later_intro. by apply const_intro.
+  Qed.
 End LiftingTests.