diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5b02c5a5fa7c793e55c7e673f4ba1c46a977a1e7..9030e40814bf1afadd8bc2fc9a5d9b974598d89b 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -24,7 +24,7 @@ Section fn.
   Global Instance fn_send E tys ty : Send (fn E tys ty).
   Proof. iIntros (tid1 tid2 vl). done. Qed.
 
-  Instance fn_contractive n' E :
+  Lemma fn_contractive n' E :
     Proper (pointwise_relation A (dist_later n') ==>
             pointwise_relation A (dist_later n') ==> dist n') (fn E).
   Proof.