From 7293e063458a0e449e2de10f7ea5f243b01e0cf7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Sep 2016 13:44:55 +0200
Subject: [PATCH] Prove always_if_pure.

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

diff --git a/algebra/upred.v b/algebra/upred.v
index d41a5adec..e9a83061b 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1081,6 +1081,9 @@ Lemma always_if_elim p P : □?p P ⊢ P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
 Lemma always_elim_if p P : □ P ⊢ □?p P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
+
+Lemma always_if_pure p φ : □?p ■ φ ⊣⊢ ■ φ.
+Proof. destruct p; simpl; auto using always_pure. Qed.
 Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
 Proof. destruct p; simpl; auto using always_and. Qed.
 Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
-- 
GitLab