diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 0214e24d5f4e28f34373e7e7d9dbb6c74ed10262..14214350793008bc921a2843d939e24ec71dc7bc 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -10,8 +10,6 @@ Set Default Proof Using "Type".
 Section refmut_functions.
   Context `{typeG Σ, refcellG Σ}.
 
-  (* TODO : map, when we will have a nice story about closures. *)
-
   (* Turning a refmut into a shared borrow. *)
   Definition refmut_deref : val :=
     funrec: <> ["x"] :=
@@ -63,7 +61,7 @@ Section refmut_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma refmut_derefmut_type ty :
-    typed_instruction_ty [] [] [] refmut_deref
+    typed_instruction_ty [] [] [] refmut_derefmut
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
           (fun '(α, β) => &uniq{α}ty)%T).