From 5657f5ca772c85f930a7e57b21644f0c515fd702 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 7 Aug 2017 00:50:35 +0200
Subject: [PATCH] sig_equivI

---
 theories/base_logic/primitive.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 7069ada48..cca9ddba1 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -592,5 +592,10 @@ Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x
 Proof. by unseal. Qed.
 Lemma cofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
+
+(* Sig ofes *)
+Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sigC P) :
+  x ≡ y ⊣⊢ proj1_sig x ≡ proj1_sig y.
+Proof. by unseal. Qed.
 End primitive.
 End uPred.
-- 
GitLab