From 66a41586e0abba4ea44c78c1d19482d03b2ff2d3 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 14 Dec 2017 09:45:20 +0100
Subject: [PATCH] Add lemma monPred_car_embed.

---
 theories/bi/monpred.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 3e6cbf6b5..e0ac53384 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -413,6 +413,10 @@ Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed
 Lemma monPred_impl_force P Q i : (P → Q) i -∗ (P i → Q i).
 Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
 
+Lemma monPred_car_embed (P : PROP) (i : I) :
+  (bi_embed (B := monPred _ _) P) i ⊣⊢ P.
+Proof. by unseal. Qed.
+
 Lemma monPred_persistently_if_eq p P i:
   (bi_persistently_if p P) i = bi_persistently_if p (P i).
 Proof. rewrite /bi_persistently_if. unseal. by destruct p. Qed.
-- 
GitLab