From 83a58304d6323c362711d03d23f94229d6caf844 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Mar 2019 14:26:15 +0100
Subject: [PATCH] Less LISP :)
---
theories/logic/model.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 0a5a020..3f88adf 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -245,8 +245,8 @@ Section monadic.
Lemma refines_bind K K' E A A' e e' :
(REL e << e' @ E : A) -∗
(∀ v v', A v v' -∗
- (REL fill K (of_val v) << fill K' (of_val v') : A')) -∗
- (REL fill K e << fill K' e' @ E : A').
+ REL fill K (of_val v) << fill K' (of_val v') : A') -∗
+ REL fill K e << fill K' e' @ E : A'.
Proof.
iIntros "Hm Hf".
rewrite refines_eq /refines_def.
--
GitLab