diff --git a/theories/logrel/F_mu_ref_conc/typing.v b/theories/logrel/F_mu_ref_conc/typing.v
index 799148654296604b19465b766a57a44951d6ab50..1af4089e31e7208a484e5fcf67fdbd990a52731d 100644
--- a/theories/logrel/F_mu_ref_conc/typing.v
+++ b/theories/logrel/F_mu_ref_conc/typing.v
@@ -147,7 +147,7 @@ Proof.
     match goal with H : context[_ → _ ⊢ₜ _ : _] |- _ => rename H into IH end.
     specialize (IH
       (subst (ren (+1)) <$> Γ1) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
-    rewrite ?map_length in IH.
+    rewrite ?length_map in IH.
     repeat rewrite fmap_app. apply IH.
     by repeat rewrite fmap_app.
   - econstructor; eauto.
@@ -155,7 +155,7 @@ Proof.
     match goal with H : context[_ → _ ⊢ₜ _ : TExist ?t] |- _ => rename t into τ end.
     specialize (IH
       (τ :: (subst (ren (+1)) <$> Γ1)) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
-    asimpl in IH. rewrite ?map_length in IH.
+    asimpl in IH. rewrite ?length_map in IH.
     repeat rewrite fmap_app. apply IH.
     by repeat rewrite fmap_app.
 Qed.