From b8dc1d84f79fe3705096e4b7bbb9d6169051f9e4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Sep 2017 19:41:22 +0200
Subject: [PATCH] Version of wp_bind_inv for ectx languages.

Typeclass search gets less confused when this version is used, also,
we had the same for `wp_bind` already.
---
 theories/program_logic/ectx_lifting.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 56bd2a267..82275d0f3 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -16,6 +16,10 @@ Lemma wp_ectx_bind {E Φ} K e :
   WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
 
+Lemma wp_ectx_bind_inv {E Φ} K e :
+  WP fill K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}.
+Proof. apply: weakestpre.wp_bind_inv. Qed.
+
 Lemma wp_lift_head_step {E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
-- 
GitLab