diff --git a/theories/logrel/F_mu_ref_conc/typing.v b/theories/logrel/F_mu_ref_conc/typing.v
index c6af41f769c82189425b319367d62abf9334b55c..abe7e7f5c95b076d2fff8031dee19f25debc950d 100644
--- a/theories/logrel/F_mu_ref_conc/typing.v
+++ b/theories/logrel/F_mu_ref_conc/typing.v
@@ -113,8 +113,8 @@ Proof.
   - rename select (_ !! _ = Some _) into H.
     apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with lia.
   - f_equal. eauto.
-  - f_equal. rewrite ->map_length in *. done.
-  - rewrite ->map_length in *; by f_equal.
+  - f_equal. rewrite ->fmap_length in *. done.
+  - rewrite ->fmap_length in *; by f_equal.
 Qed.
 
 (** Weakening *)