diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index be34421cd08f69ae4577661b3a0af512673d3800..3136bd97703ec6797e49702d179562465b176aa5 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -192,8 +192,8 @@ Section code.
       delete [ #1; "g"];; return: ["r"].
 
   Lemma mutexguard_derefmut_type ty `{!TyWf ty} :
-    typed_val mutexguard_derefmut (fn (fun '(α, β) =>
-      FP_wf ∅ [# &uniq{α}(mutexguard β ty)]%T (&uniq{α}ty)%T)).
+    typed_val mutexguard_derefmut
+              (fn(∀ '(α, β), ∅; &uniq{α}(mutexguard β ty)) → &uniq{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
@@ -234,8 +234,8 @@ Section code.
   Definition mutexguard_deref : val := mutexguard_derefmut.
 
   Lemma mutexguard_deref_type ty `{!TyWf ty} :
-    typed_val mutexguard_derefmut (fn (fun '(α, β) =>
-      FP_wf ∅ [# &shr{α}(mutexguard β ty)]%T (&shr{α}ty)%T)).
+    typed_val mutexguard_derefmut
+              (fn(∀ '(α, β), ∅; &shr{α}(mutexguard β ty)) → &shr{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 95ee3e023ceb230cc1147a7b47b7bf055b40f780..84f92f9e5fb31bbb7d5972ae755ead2a08d3be0a 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -45,8 +45,6 @@ Section ref_functions.
       letalloc: "r" <-{2} !"x'" in
       delete [ #1; "x"];; return: ["r"].
 
-  (* FIXME : using λ instead of fun triggers an anomaly.
-     See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
   Lemma ref_clone_type ty `{!TyWf ty} :
     typed_val ref_clone (fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → ref β ty).
 
@@ -110,7 +108,7 @@ Section ref_functions.
 
   Lemma ref_deref_type ty `{!TyWf ty} :
     typed_val ref_deref
-      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+      (fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → &shr{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 82fa6c8d5d758ff3f7330ad748a58bcd0c5af3f2..89c81f6b721968d6f47983bfc821aaf435317512 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -19,8 +19,7 @@ Section refmut_functions.
       delete [ #1; "x"];; return: ["r"].
 
   Lemma refmut_deref_type ty `{!TyWf ty} :
-    typed_val refmut_deref (fn (fun '(α, β) =>
-       FP_wf ∅ [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
+    typed_val refmut_deref (fn(∀ '(α, β), ∅; &shr{α}(refmut β ty)) → &shr{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -57,9 +56,9 @@ Section refmut_functions.
   Definition refmut_derefmut : val := refmut_deref.
 
   Lemma refmut_derefmut_type ty `{!TyWf ty} :
-    typed_val refmut_derefmut (fn (fun '(α, β) =>
-      FP_wf ∅ [# &uniq{α}(refmut β ty)]%T (&uniq{α}ty)%T)).
-   Proof.
+    typed_val refmut_derefmut
+              (fn(∀ '(α, β), ∅; &uniq{α}(refmut β ty)) → &uniq{α}ty).
+  Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').