From c9261672d4cb54fa3bd534212b371126ede48850 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Feb 2016 16:42:06 +0100
Subject: [PATCH] Lemma about wand.

---
 algebra/upred.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/algebra/upred.v b/algebra/upred.v
index a8ce1ad7b..f18d8e31b 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -670,6 +670,8 @@ Proof.
   apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
   apply sep_mono_r, wand_elim_r.
 Qed.
+Lemma wand_diag P : (P -★ P)%I ≡ True%I.
+Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
 Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).
-- 
GitLab