From b624d134820e2cf0b30f27148d8d661566bcde9f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Mar 2019 20:08:10 +0100
Subject: [PATCH] Make proof of `least_fixpoint_unfold_2` more readable by
including a `simple`.
---
theories/bi/lib/fixpoint.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 975266f3f..0e4506f11 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -45,7 +45,7 @@ Section least.
bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
Proof.
iIntros "HF". iApply ("HF" $! (CofeMor (F (bi_least_fixpoint F))) with "[#]").
- iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#]"); last done.
+ iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
iIntros "!#" (z) "?". by iApply least_fixpoint_unfold_2.
Qed.
--
GitLab