From 31321366ed477f9be3847c7d37eb5d9da41258f6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 30 Jan 2016 17:58:54 +0100
Subject: [PATCH] demonstrate the folding problem

---
 barrier/tests.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/barrier/tests.v b/barrier/tests.v
index 32a2d738a..499f9351b 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.
-- 
GitLab