From 225cac4f419106eb813b0f4345a0cd5098d6f68a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 6 Apr 2020 16:50:07 +0200
Subject: [PATCH] Simplify proof of `wp_lift_step_fupd`.

---
 theories/program_logic/lifting.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index f560a780b..96118502d 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -22,11 +22,7 @@ Lemma wp_lift_step_fupd s E Φ e1 :
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
-Proof.
-  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
-  iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s.
-  iIntros (????). iApply "H". eauto.
-Qed.
+Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
 
 Lemma wp_lift_stuck E Φ e :
   to_val e = None →
-- 
GitLab