From 270dca69ca90c62e9a9ca1974912a2d78ba9d1c4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 15:38:53 +0200
Subject: [PATCH] Separable instance for `internal_eq`.

---
 iris/bi/internal_eq.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 796aa71d5..4f19ba89b 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -230,6 +230,15 @@ Section internal_eq_derived.
     Persistent (PROP:=PROP) (a ≡ b).
   Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 
+  Global Instance internal_eq_separable {A : ofe} (a b : A) :
+    Separable (PROP:=PROP) (a ≡ b).
+  Proof.
+    intros Q. rewrite absorbingly_internal_eq.
+    apply (internal_eq_rewrite' a b (λ b', <affine> (a ≡ b') ∗ Q)%I); auto.
+    rewrite and_elim_r -(equiv_internal_eq True) //.
+    by rewrite affinely_True_emp left_id.
+  Qed.
+
   (* Equality under a later. *)
   Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
     {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
-- 
GitLab