From 126d54c3723f5e7eb4d0a5b901963c719b17078a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 6 Oct 2016 00:24:43 +0200
Subject: [PATCH] Internalized versions of the equality on funC and morC.

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

diff --git a/algebra/upred.v b/algebra/upred.v
index 5005e73cf..a0b707174 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1361,6 +1361,12 @@ Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. uPred.unseal. by destruct mx. Qed.
 
+(* Functions *)
+Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof. by uPred.unseal. Qed.
+Lemma cofe_moreC_equivI {A B : cofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof. by uPred.unseal. Qed.
+
 (* Timeless instances *)
 Global Instance pure_timeless φ : TimelessP (■ φ : uPred M)%I.
 Proof.
-- 
GitLab