diff --git a/theories/typing/function.v b/theories/typing/function.v
index 9f9b9bcbdb06ea8246da81f81b9dc597425e1bdf..b09e8af19d3c4cdce5a834ec74a6f9f55d3517fb 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -98,6 +98,12 @@ End fn.
 
 Arguments fn_params {_ _} _.
 
+(* The parameter of [FP] are in the wrong order in order to make sure
+   that type-checking is done in that order, so that the [ELCtx_Alive]
+   is taken as a coercion. We reestablish the intuitive order with
+   [FP'] *)
+Notation FP' E tys ty := (FP tys ty E).
+
 (* We use recursive notation for binders as well, to allow patterns
    like '(a, b) to be used. In practice, only one binder is ever used,
    but using recursive binders is the only way to make Coq accept
@@ -106,19 +112,19 @@ Arguments fn_params {_ _} _.
    printing. Once on 8.6pl1, this should work.  *)
 Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
   (fn (λ x, (.. (λ x',
-      FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T E%EL)..)))
+      FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
   (at level 99, R at level 200, x binder, x' binder,
    format "'fn(∀'  x .. x' ','  E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
-  (fn (λ x, (.. (λ x', FP Vector.nil R%T E%EL)..)))
+  (fn (λ x, (.. (λ x', FP' E%EL Vector.nil R%T)..)))
   (at level 99, R at level 200, x binder, x' binder,
    format "'fn(∀'  x .. x' ','  E ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
-  (fn (λ _:(), FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T E%EL) )
+  (fn (λ _:(), FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
   (at level 99, R at level 200,
    format "'fn(' E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ')' '→' R" :=
-  (fn (λ _:(), FP Vector.nil R%T E%EL))
+  (fn (λ _:(), FP' E%EL Vector.nil R%T))
   (at level 99, R at level 200,
    format "'fn(' E ')'  '→'  R") : lrust_type_scope.
 
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 0d18dc23ef8685b56d48901aaf4f1a150e23de7d..b0dc67a558d4accbdd0ba5fb31421beda63448f4 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,8 +11,8 @@ Section fake_shared_box.
 
   Lemma cell_replace_type ty :
     typed_val fake_shared_box
-      (fn (fun '(α, β) => FP [# &shr{α}(&shr{β} ty)]
-                             (&shr{α}box ty) [α; β; α ⊑ β]%EL)).
+      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+                              [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index fd406c49bdaf3f6c547b010fda2c720560373cbd..c1012db9e85a6547a405cad6804de80b72e5f486 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -56,7 +56,7 @@ Section ref_functions.
      See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
   Lemma ref_clone_type ty :
     typed_val ref_clone
-      (fn (fun '(α, β) => FP [# &shr{α}(ref β ty)]%T (ref β ty)%T [α; β]%EL)).
+      (fn (fun '(α, β) => FP' [α; β]%EL [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -116,7 +116,7 @@ Section ref_functions.
 
   Lemma ref_deref_type ty :
     typed_val ref_deref
-      (fn (fun '(α, β) => FP [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T [α; β; α ⊑ β]%EL)).
+      (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.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 07088ab1e6ef453783c877469d3c7cbd1c452f1c..8c6fd2351e90af488c32071ee188e05e3cff6be5 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -20,7 +20,7 @@ Section refmut_functions.
 
   Lemma refmut_deref_type ty :
     typed_val refmut_deref
-      (fn (fun '(α, β) => FP [# &shr{α}(refmut β ty)]%T (&shr{α}ty) [α; β; α ⊑ β]%EL)).
+      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -60,9 +60,9 @@ Section refmut_functions.
 
   Lemma refmut_derefmut_type ty :
     typed_val refmut_derefmut
-      (fn (fun '(α, β) => FP [# &uniq{α}(refmut β ty)]%T
-                             (&uniq{α}ty)%T [α; β; α ⊑ β]%EL)).
-  Proof.
+      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &uniq{α}(refmut β ty)]%T
+                              (&uniq{α}ty)%T)).
+   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index d76e2b77fcbe14cf45e64b603c08902c73ebf536..c2eaab6779ab658e48c8efbb1cead75bd23504ee 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,8 +20,8 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_deref_type ty :
     typed_val rwlockreadguard_deref
-      (fn (fun '(α, β) => FP [# &shr{α}(rwlockreadguard β ty)]
-                             (&shr{α}ty) [α; β; α ⊑ β]%EL)).
+      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+                              [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 3e3d4ee0bbfc70551ea9a3af8f7926c796dd4348..0ebe26120cc2200c39602b83bc33c2b6eb33e077 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,9 +20,8 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_deref_type ty :
     typed_val rwlockwriteguard_deref
-      (fn (fun '(α, β) => FP [# &shr{α}(rwlockwriteguard β ty)]
-                             (&shr{α}ty)
-                             [α; β; α ⊑ β]%EL)).
+      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+                              [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -63,9 +62,8 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_derefmut_type ty :
     typed_val rwlockwriteguard_derefmut
-      (fn (fun '(α, β) => FP [# &uniq{α}(rwlockwriteguard β ty)]
-                             (&uniq{α}ty)
-                             [α; β; α ⊑ β]%EL)).
+      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+                              [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 45cf25e5bbddca11c8f96277a1a7ce20cb890fc1..e19b166b782ef60d39631fe302502b7a7ba0bf86 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -84,7 +84,7 @@ Section spawn.
         iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
       (* FIXME this is horrible. *)
-      assert (Hcall := type_call' [] [] [] f' [env:expr] (λ _:(), FP [# envty] retty [])).
+      assert (Hcall := type_call' [] [] [] f' [env:expr] (λ _:(), FP' [] [# envty] retty)).
       specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
       erewrite of_val_unlock in Hcall; last done.
       iApply (Hcall $! _ 1%Qp with "LFT Htl [] [] [Hfin]").