From 1addf2ac04a252ad0623d790f7517a830e88a77e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 27 Jan 2018 19:05:23 +0100
Subject: [PATCH] Support framing pure facts and equalities under an embedding.

---
 theories/proofmode/class_instances.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 56c22f0e3..fb9522f0d 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -838,6 +838,13 @@ Proof.
   rewrite /Frame /MakeEmbed => <- <-.
   rewrite bi_embed_sep bi_embed_affinely_if bi_embed_persistently_if => //.
 Qed.
+Global Instance frame_pure_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') φ :
+  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q'.
+Proof. rewrite /Frame /MakeEmbed -bi_embed_pure. apply (frame_embed p P Q). Qed.
+Global Instance frame_eq_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP')
+       {A : ofeT} (a b : A) :
+  Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
+Proof. rewrite /Frame /MakeEmbed -bi_embed_internal_eq. apply (frame_embed p P Q). Qed.
 
 Class MakeSep (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ.
 Arguments MakeSep _%I _%I _%I.
-- 
GitLab