diff --git a/algebra/upred.v b/algebra/upred.v
index 5005e73cf4b3d9d881110f7ea9ad6554bfdf1a16..a0b70717465f4bd0844d2286384e8737ff29a7fc 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.