diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 7069ada4878ec08b23c761e38a8a60f9a5dfa5c7..cca9ddba1b377204d3f068f984bf4d678b3229a1 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.