diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index b0dc67a558d4accbdd0ba5fb31421beda63448f4..82ef21c14a8a6ef624da8c5dd7f6b76319dc17a8 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,7 +11,7 @@ Section fake_shared_box.
 
   Lemma cell_replace_type ty :
     typed_val fake_shared_box
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
                               [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 1799970be091d82f24e52eee5eae3003d46000eb..e157512661ee7d7f58c39a3a06031cba8f6ff1d6 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -116,7 +116,7 @@ Section ref_functions.
 
   Lemma ref_deref_type ty :
     typed_val ref_deref
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.