From 3c9e8424ad07bc3b29eedfbc371e28e9011aea6e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 11 Feb 2020 17:28:08 +0100
Subject: [PATCH] Write `twp_ind` in a more sane way.

---
 theories/program_logic/total_weakestpre.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index a08d64085..f2bbcae8c 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -77,8 +77,8 @@ Lemma twp_unfold s E e Φ : WP e @ s; E [{ Φ }] ⊣⊢ twp_pre s (twp s) E e Φ
 Proof. by rewrite twp_eq /twp_def least_fixpoint_unfold. Qed.
 Lemma twp_ind s Ψ :
   (∀ n E e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) →
-  (□ (∀ e E Φ, twp_pre s (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) →
-  ∀ e E Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ)%I.
+  □ (∀ e E Φ, twp_pre s (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) -∗
+  ∀ e E Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ.
 Proof.
   iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
   set (Ψ' := curry3 Ψ :
-- 
GitLab