diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 99ceda8626896827b87f2f7b34229e80cc42767e..1eabd4e3b07504b63bc5d67d016c50a7ce5096ee 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,7 @@ Section get_x.
        delete [ #1; "p"] ;; "return" ["r"].
 
   Lemma get_x_type :
-    typed_val get_x (fn(∀ α, [☀α]; &uniq{α} Π[int; int]) → &shr{α} int).
+    typed_val get_x (fn(∀ α, [α]; &uniq{α} Π[int; int]) → &shr{α} int).
   (* FIXME: The above is pretty-printed with some explicit scope annotations,
      and without using 'typed_instruction_ty'.  I think that's related to
      the list notation that we added to %TC. *)
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index f1e7aaa443fdd1ca5991d043b96d1290a17dd313..b9b5734349158ee2b98410293564479866e26e48 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,7 +12,7 @@ Section unbox.
        delete [ #1; "b"] ;; "return" ["r"].
 
   Lemma ubox_type :
-    typed_val unbox (fn(∀ α, [☀α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
+    typed_val unbox (fn(∀ α, [α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret b).
       inv_vec b=>b. simpl_subst.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index eb1d163e141832ab4309373a00c1262b558759db..a974acf83722c6e3f6a4c43a84d18b385fec5c42 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -8,40 +8,66 @@ Set Default Proof Using "Type".
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
 
-  Program Definition fn (E : A → elctx)
-          (tys : A → vec type n) (ty : A → type) : type :=
+  Record fn_params := FP { fp_tys : vec type n; fp_ty : type; fp_E : elctx }.
+
+  Program Definition fn (fp : A → fn_params) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
          ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
-            â–¡ typed_body (E x) []
-                         [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
+            â–¡ typed_body (fp x).(fp_E) []
+                         [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                          (zip_with (TCtx_hasty ∘ of_val) xl
-                                   (box <$> (vec_to_list (tys x))))
+                                   (box <$> (vec_to_list (fp x).(fp_tys))))
                          (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
   Next Obligation.
-    iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
+    iIntros (fp tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
   Qed.
 
-  Global Instance fn_send E tys ty : Send (fn E tys ty).
+  Global Instance fn_send fp : Send (fn fp).
   Proof. iIntros (tid1 tid2 vl). done. Qed.
 
-  Lemma fn_type_contractive n' E :
-    Proper (pointwise_relation A (B := vec type n) (Forall2 (type_dist2_later n')) ==>
-            pointwise_relation A (type_dist2_later n') ==> type_dist2 n') (fn E).
+  Definition fn_params_rel (ty_rel : relation type) : relation fn_params :=
+    λ fp1 fp2,
+      Forall2 ty_rel fp2.(fp_tys) fp1.(fp_tys) ∧ ty_rel fp1.(fp_ty) fp2.(fp_ty) ∧
+      fp1.(fp_E) = fp2.(fp_E).
+
+  Global Instance fp_tys_proper R :
+    Proper (flip (fn_params_rel R) ==> (Forall2 R : relation (vec _ _))) fp_tys.
+  Proof. intros ?? HR. apply HR. Qed.
+  Global Instance fp_tys_proper_flip R :
+    Proper (fn_params_rel R ==> flip (Forall2 R : relation (vec _ _))) fp_tys.
+  Proof. intros ?? HR. apply HR. Qed.
+
+  Global Instance fp_ty_proper R :
+    Proper (fn_params_rel R ==> R) fp_ty.
+  Proof. intros ?? HR. apply HR. Qed.
+
+  Global Instance fp_E_proper R :
+    Proper (fn_params_rel R ==> eq) fp_E.
+  Proof. intros ?? HR. apply HR. Qed.
+
+  Global Instance FP_proper R :
+    Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==> eq ==> fn_params_rel R) FP.
+  Proof. by split; [|split]. Qed.
+
+  Global Instance fn_type_contractive n' :
+    Proper (pointwise_relation A (fn_params_rel (type_dist2_later n')) ==>
+            type_dist2 n') fn.
   Proof.
-    intros ?? Htys ?? Hty. apply ty_of_st_type_ne. destruct n'; first done.
+    intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
     constructor; simpl.
     (* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
     (* The clean way to do this would be to have a metric on type contexts. Oh well. *)
     intros tid vl. unfold typed_body.
-    do 12 f_equiv. f_contractive. do 17 f_equiv.
+    do 12 f_equiv. f_contractive. do 17 (apply Hfp || f_equiv).
+    - f_equiv. apply Hfp.
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hty || f_equiv).
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hfp || f_equiv).
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
       cut (∀ n tid p i, Proper (dist n ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
-        - eapply Forall2_impl; first exact: Htys. intros.
+        - symmetry. eapply Forall2_impl; first apply Hfp. intros.
           apply dist_later_dist, type_dist2_dist_later. done.
         - apply _. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
@@ -57,52 +83,54 @@ Section fn.
         * iIntros "H". by iApply "H".
         * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
   Qed.
-  Global Existing Instance fn_type_contractive.
 
-  Global Instance fn_ne n' E :
-    Proper (pointwise_relation A (dist n') ==>
-            pointwise_relation A (dist n') ==> dist n') (fn E).
+  Global Instance fn_ne n' :
+    Proper (pointwise_relation A (fn_params_rel (dist n')) ==> dist n') fn.
   Proof.
-    intros ?? H1 ?? H2. apply dist_later_dist, type_dist2_dist_later.
-    apply fn_type_contractive=>u; simpl.
-    - eapply Forall2_impl; first exact: H1. intros. simpl.
+    intros ?? Hfp. apply dist_later_dist, type_dist2_dist_later.
+    apply fn_type_contractive=>u. split; last split.
+    - eapply Forall2_impl; first apply Hfp. intros. simpl.
       apply type_dist_dist2. done.
-    - apply type_dist_dist2. apply H2.
+    - apply type_dist_dist2. apply Hfp.
+    - apply Hfp.
   Qed.
 End fn.
 
+Arguments fn_params {_ _} _.
+
 (* TODO: Once we depend on 8.6pl1, extend this to recursive binders so that
    patterns like '(a, b) can be used. *)
 Notation "'fn(∀' x ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
-  (fn (λ x, E%EL) (λ x, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ x, R%T))
+  (fn (λ x, FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T E%EL))
   (at level 99, R at level 200,
    format "'fn(∀' x ','  E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(∀' x ',' E ')' '→' R" :=
-  (fn (λ x, E%EL) (λ x, Vector.nil) (λ x, R%T))
+  (fn (λ x, FP Vector.nil R%T E%EL))
   (at level 99, R at level 200,
    format "'fn(∀' x ','  E ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
-  (fn (λ _:(), E%EL) (λ _, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ _, R%T))
+  (fn (λ _:(), FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T E%EL) )
   (at level 99, R at level 200,
    format "'fn(' E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ')' '→' R" :=
-  (fn (λ _:(), E%EL) (λ _, Vector.nil) (λ _, R%T))
+  (fn (λ _:(), FP Vector.nil R%T E%EL))
   (at level 99, R at level 200,
    format "'fn(' E ')'  '→'  R") : lrust_type_scope.
 
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma fn_subtype_full {A n} E0 L0 E E' (tys tys' : A → vec type n) ty ty' :
-    (∀ x, elctx_incl E0 L0 (E x) (E' x)) →
-    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys' x) (tys x)) →
-    (∀ x, subtype (E0 ++ E x) L0 (ty x) (ty' x)) →
-    subtype E0 L0 (fn E' tys ty) (fn E tys' ty').
+  Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
+    (∀ x, elctx_incl E0 L0 (fp' x).(fp_E) (fp x).(fp_E)) →
+    (∀ x, Forall2 (subtype (E0 ++ (fp' x).(fp_E)) L0)
+                  (fp' x).(fp_tys) (fp x).(fp_tys)) →
+    (∀ x, subtype (E0 ++ (fp' x).(fp_E)) L0 (fp x).(fp_ty) (fp' x).(fp_ty)) →
+    subtype E0 L0 (fn fp) (fn fp').
   Proof.
     intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
     iIntros "#HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
     iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
-    rewrite /typed_body. iIntros "* !# * #LFT Htl HE HL HC HT".
+    rewrite /typed_body. iIntros (x k xl) "!# * #LFT Htl HE HL HC HT".
     iDestruct (elctx_interp_persist with "HE") as "#HEp".
     iMod (HE with "HE0 HL0 HE") as (qE') "[HE' Hclose]". done.
     iApply ("Hf" with "LFT Htl HE' HL [HC Hclose] [HT]").
@@ -114,14 +142,15 @@ Section typing.
       { by apply elem_of_list_singleton. }
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
-      assert (Hst : subtype (E0 ++ E x) L0 (box (ty x)) (box (ty' x)))
+      assert (Hst : subtype (E0 ++ (fp' x).(fp_E)) L0
+                            (box (fp x).(fp_ty)) (box (fp' x).(fp_ty)))
         by by rewrite ->Hty.
       iDestruct (Hst with "[HE0 HEp] HL0") as "(_ & Hty & _)".
       { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
       by iApply "Hty".
     - rewrite /tctx_interp
-         -(fst_zip (tys x) (tys' x)) ?vec_to_list_length //
-         -{1}(snd_zip (tys x) (tys' x)) ?vec_to_list_length //
+         -(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
+         -{1}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
          !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
       iApply big_sepL_impl. iSplit; last done. iIntros "{HT}!#".
       iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
@@ -129,58 +158,43 @@ Section typing.
       rewrite !lookup_zip_with.
       iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
         (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
-      specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
-      assert (Hst : subtype (E0 ++ E x) L0 (box ty2') (box ty1'))
+      eapply Forall2_lookup_lr in Htys; try done.
+      assert (Hst : subtype (E0 ++ (fp' x).(fp_E)) L0 (box ty2') (box ty1'))
         by by rewrite ->Htys.
       iDestruct (Hst with "[] []") as "(_ & #Ho & _)"; [ |done|].
       { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
       by iApply "Ho".
   Qed.
 
-  Lemma fn_subtype_ty {A n} E0 L0 E (tys1 tys2 : A → vec type n) ty1 ty2 :
-    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x) (tys1 x)) →
-    (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
-    subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
-  Proof. intros. by apply fn_subtype_full. Qed.
-
   (* This proper and the next can probably not be inferred, but oh well. *)
-  Global Instance fn_subtype_ty' {A n} E0 L0 E :
-    Proper (flip (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (subtype E0 L0) v1 v2)) ==>
-            pointwise_relation A (subtype E0 L0) ==> subtype E0 L0) (fn E).
+  Global Instance fn_subtype' {A n} E0 L0 :
+    Proper (pointwise_relation A (fn_params_rel (n:=n) (subtype E0 L0)) ==>
+            subtype E0 L0) fn.
   Proof.
-    intros tys1 tys2 Htys ty1 ty2 Hty. apply fn_subtype_ty.
-    - intros. eapply Forall2_impl; first eapply Htys. intros ??.
+    intros fp1 fp2 Hfp. apply fn_subtype=>x; destruct (Hfp x) as (Htys & Hty & HE).
+    - by rewrite HE.
+    - eapply Forall2_impl; first eapply Htys. intros ??.
       eapply subtype_weaken; last done. by apply submseteq_inserts_r.
-    - intros. eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
-  Qed.
-
-  Global Instance fn_eqtype_ty' {A n} E0 L0 E :
-    Proper (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (eqtype E0 L0) v1 v2) ==>
-            pointwise_relation A (eqtype E0 L0) ==> eqtype E0 L0) (fn E).
-  Proof.
-    intros tys1 tys2 Htys ty1 ty2 Hty. split; eapply fn_subtype_ty'; try (by intro; apply Hty);
-      intros x; (apply Forall2_flip + idtac); (eapply Forall2_impl; first by eapply (Htys x)); by intros ??[].
-  Qed.
-
-  Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
-    (∀ x, elctx_sat (E x) [] (E' x)) →
-    subtype E0 L0 (fn E' tys ty) (fn E tys ty).
-  Proof.
-    intros. apply fn_subtype_full; try done. by intros; apply elctx_sat_incl.
+    - eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
   Qed.
 
-  Lemma fn_subtype_lft_incl {A n} E0 L0 E κ κ' (tys : A → vec type n) ty :
-    lctx_lft_incl E0 L0 κ κ' →
-    subtype E0 L0 (fn (λ x, (κ ⊑ κ') :: E x)%EL tys ty) (fn E tys ty).
+  Global Instance fn_eqtype' {A n} E0 L0 :
+    Proper (pointwise_relation A (fn_params_rel (n:=n) (eqtype E0 L0)) ==>
+            eqtype E0 L0) fn.
   Proof.
-    intros Hκκ'. apply fn_subtype_full; try done. intros.
-    apply elctx_incl_lft_incl; last by apply elctx_incl_refl.
-    iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL").
-    rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[$ _]".
+    intros fp1 fp2 Hfp. split; eapply fn_subtype=>x; destruct (Hfp x) as (Htys & Hty & HE).
+    - by rewrite HE.
+    - eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
+      eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
+    - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
+    - by rewrite HE.
+    - symmetry in Htys. eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
+      eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
+    - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
   Qed.
 
-  Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :
-    subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
+  Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 fp :
+    subtype E0 L0 (fn (n:=n) fp) (fn (fp ∘ σ)).
   Proof.
     apply subtype_simple_type=>//= _ vl.
     iIntros "_ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
@@ -188,12 +202,12 @@ Section typing.
     rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
   Qed.
 
-  Lemma type_call' {A} E L E' T p (ps : list path)
-                         (tys : A → vec type (length ps)) ty k x :
-    elctx_sat E L (E' x) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (ty x)) :: T)]
-               ((p ◁ fn E' tys ty) ::
-                zip_with TCtx_hasty ps (box <$> (vec_to_list (tys x))) ++
+  Lemma type_call' {A} E L T p (ps : list path)
+                         (fp : A → fn_params (length ps)) k x :
+    elctx_sat E L (fp x).(fp_E) →
+    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
+               ((p ◁ fn fp) ::
+                zip_with TCtx_hasty ps (box <$> (vec_to_list (fp x).(fp_tys))) ++
                 T)
                (call: p ps → k).
   Proof.
@@ -201,10 +215,10 @@ Section typing.
     rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
     wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
-               vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (tys x))%I
+               vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
             with "[Hargs]"); first wp_done.
     - rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
-      clear dependent ty k p.
+      clear dependent k p.
       rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
               (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
       iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
@@ -212,8 +226,8 @@ Section typing.
     - simpl. change (@length expr ps) with (length ps).
       iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
       iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
-      iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl tys.
-      rewrite <-EQl=>vl tys. iApply wp_rec; try done.
+      iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl fp HE.
+      rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
       { rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
       { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
       iNext. iSpecialize ("Hf" $! x k vl).
@@ -231,14 +245,14 @@ Section typing.
         iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
   Qed.
 
-  Lemma type_call {A} x E L E' C T T' T'' p (ps : list path)
-                        (tys : A → vec type (length ps)) ty k :
-    (p ◁ fn E' tys ty)%TC ∈ T →
-    elctx_sat E L (E' x) →
+  Lemma type_call {A} x E L C T T' T'' p (ps : list path)
+                        (fp : A → fn_params (length ps)) k :
+    (p ◁ fn fp)%TC ∈ T →
+    elctx_sat E L (fp x).(fp_E) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
-                                   (box <$> vec_to_list (tys x))) T T' →
+                                   (box <$> vec_to_list (fp x).(fp_tys))) T T' →
     (k ◁cont(L, T''))%CC ∈ C →
-    (∀ ret : val, tctx_incl E L ((ret ◁ box (ty x))::T') (T'' [# ret])) →
+    (∀ ret : val, tctx_incl E L ((ret ◁ box (fp x).(fp_ty))::T') (T'' [# ret])) →
     typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HE HTT' HC HT'T''.
@@ -249,18 +263,18 @@ Section typing.
       apply copy_elem_of_tctx_incl; last done. apply _.
   Qed.
 
-  Lemma type_letcall {A} x E L E' C T T' p (ps : list path)
-                        (tys : A → vec type (length ps)) ty b e :
+  Lemma type_letcall {A} x E L C T T' p (ps : list path)
+                        (fp : A → fn_params (length ps)) b e :
     Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
-    (p ◁ fn E' tys ty)%TC ∈ T →
-    elctx_sat E L (E' x) →
+    (p ◁ fn fp)%TC ∈ T →
+    elctx_sat E L (fp x).(fp_E) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
-                                   (box <$> vec_to_list (tys x))) T T' →
-    (∀ ret : val, typed_body E L C ((ret ◁ box (ty x))::T') (subst' b ret e)) -∗
+                                   (box <$> vec_to_list (fp x).(fp_tys))) T T' →
+    (∀ ret : val, typed_body E L C ((ret ◁ box (fp x).(fp_ty))::T') (subst' b ret e)) -∗
     typed_body E L C T (letcall: b := p ps in e).
   Proof.
     iIntros (?? Hpsc ???) "He".
-    iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (ty x)) :: T')%TC).
+    iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (fp x).(fp_ty)) :: T')%TC).
     - (* TODO : make [solve_closed] work here. *)
       eapply is_closed_weaken; first done. set_solver+.
     - (* TODO : make [solve_closed] work here. *)
@@ -283,19 +297,19 @@ Section typing.
       apply incl_cctx_incl. set_solver+.
   Qed.
 
-  Lemma type_rec {A} E L E' fb (argsb : list binder) ef e n
-        (tys : A → vec type n) ty
-        T `{!CopyC T, !SendC T} :
+  Lemma type_rec {A} E L fb (argsb : list binder) ef e n
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T} :
     ef = (funrec: fb argsb := e)%E →
     n = length argsb →
     Closed (fb :b: "return" :b: argsb +b+ []) e →
     □ (∀ x (f : val) k (args : vec val (length argsb)),
-          typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
-                     ((f ◁ fn E' tys ty) ::
+          typed_body (fp x).(fp_E) []
+                     [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                     ((f ◁ fn fp) ::
                         zip_with (TCtx_hasty ∘ of_val) args
-                                 (box <$> vec_to_list (tys x)) ++ T)
+                                 (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
                      (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
-    typed_instruction_ty E L T ef (fn E' tys ty).
+    typed_instruction_ty E L T ef (fn fp).
   Proof.
     iIntros (-> -> Hc) "#Hbody". iIntros (tid qE) " #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite ->(decide_left Hc). done. }
@@ -308,23 +322,23 @@ Section typing.
     by iApply sendc_change_tid.
   Qed.
 
-  Lemma type_fn {A} E L E' (argsb : list binder) ef e n
-        (tys : A → vec type n) ty
-        T `{!CopyC T, !SendC T} :
+  Lemma type_fn {A} E L (argsb : list binder) ef e n
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T} :
     ef = (funrec: <> argsb := e)%E →
     n = length argsb →
     Closed ("return" :b: argsb +b+ []) e →
     □ (∀ x k (args : vec val (length argsb)),
-        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
+        typed_body (fp x).(fp_E) []
+                   [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
-                             (box <$> vec_to_list (tys x)) ++ T)
+                             (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
-    typed_instruction_ty E L T ef (fn E' tys ty).
+    typed_instruction_ty E L T ef (fn fp).
   Proof.
     iIntros (???) "#He". iApply type_rec; try done. iIntros "!# *".
-    (iApply typed_body_mono; last by iApply "He"); try done.
+    iApply typed_body_mono; last iApply "He"; try done.
     eapply contains_tctx_incl. by constructor.
   Qed.
 End typing.
 
-Hint Resolve fn_subtype_full : lrust_typing.
+Hint Resolve fn_subtype : lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index b03a8fe8cc48c57d94f7972ecf7a99e38233dcc7..9ee1956b82c9f16dd453f4d91a7a73a1cfaeb6d2 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -16,7 +16,7 @@ Delimit Scope lrust_elctx_scope with EL.
    notations, so we have to use [Arguments] everywhere. *)
 Bind Scope lrust_elctx_scope with elctx_elt.
 
-Notation "☀ κ" := (ELCtx_Alive κ) (at level 70) : lrust_elctx_scope.
+Coercion ELCtx_Alive : lft >-> elctx_elt.
 Infix "⊑" := ELCtx_Incl (at level 70) : lrust_elctx_scope.
 
 Notation "a :: b" := (@cons elctx_elt a%EL b%EL)
@@ -48,7 +48,7 @@ Section lft_contexts.
   (* External lifetime contexts. *)
   Definition elctx_elt_interp (x : elctx_elt) (q : Qp) : iProp Σ :=
     match x with
-    | ☀ κ => q.[κ]%I
+    | ELCtx_Alive κ => q.[κ]%I
     | κ ⊑ κ' => (κ ⊑ κ')%I
     end%EL.
   Global Instance elctx_elt_interp_fractional x:
@@ -57,7 +57,7 @@ Section lft_contexts.
   Typeclasses Opaque elctx_elt_interp.
   Definition elctx_elt_interp_0 (x : elctx_elt) : iProp Σ :=
     match x with
-    | ☀ κ => True%I
+    | ELCtx_Alive κ => True%I
     | κ ⊑ κ' => (κ ⊑ κ')%I
     end%EL.
   Global Instance elctx_elt_interp_0_persistent x:
@@ -270,7 +270,7 @@ Section lft_contexts.
     rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
   Qed.
 
-  Lemma lctx_lft_alive_external κ: (☀κ)%EL ∈ E → lctx_lft_alive κ.
+  Lemma lctx_lft_alive_external κ: (ELCtx_Alive κ) ∈ E → lctx_lft_alive κ.
   Proof.
     iIntros ([i HE]%elem_of_list_lookup_1 F qE qL ?) "HE $ !>".
     rewrite /elctx_interp /elctx_elt_interp.
@@ -291,7 +291,7 @@ Section lft_contexts.
   Qed.
 
   Lemma lctx_lft_alive_external' κ κ':
-    (☀κ)%EL ∈ E → (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ'.
+    (ELCtx_Alive κ) ∈ E → (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ'.
   Proof.
     intros. eapply lctx_lft_alive_incl, lctx_lft_incl_external; last done.
     by apply lctx_lft_alive_external.
@@ -310,7 +310,7 @@ Section lft_contexts.
   Qed.
 
   Lemma elctx_sat_alive E' κ :
-    lctx_lft_alive κ → elctx_sat E' → elctx_sat ((☀κ) :: E')%EL.
+    lctx_lft_alive κ → elctx_sat E' → elctx_sat (κ :: E')%EL.
   Proof.
     iIntros (Hκ HE' qE qL F ?) "[HE1 HE2] [HL1 HL2]".
     iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
@@ -430,7 +430,7 @@ Section elctx_incl.
    Qed.
 
   Lemma elctx_incl_lft_alive E1 E2 κ :
-    lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
+    lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 (κ :: E2).
   Proof.
     intros Hκ HE2. rewrite (elctx_incl_dup E1).
     apply (elctx_incl_app_proper _ [_]); last done.
@@ -481,7 +481,7 @@ Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
 
 Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
   lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
-  elctx_incl E L ((☀κ) :: E1) ((☀κ') :: E2).
+  elctx_incl E L (κ :: E1) (κ' :: E2).
 Proof.
   move=> ? /elctx_incl_lft_incl -> //.
   apply (elctx_incl_app_proper _ _ [_; _] [_]); solve_typing.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index dcbc8431edb0c9147f19048fbaf03ac433204be9..bfbe7e4a91905491e35bf52c7e601dbf53a4a711 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -109,7 +109,7 @@ Section typing.
     funrec: <> ["x"] := "return" ["x"].
 
   Lemma cell_get_mut_type ty :
-    typed_val cell_get_mut (fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
+    typed_val cell_get_mut (fn(∀ α, [α]; &uniq{α} (cell ty)) → &uniq{α} ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -126,7 +126,7 @@ Section typing.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma cell_get_type `(!Copy ty) :
-    typed_val (cell_get ty) (fn(∀ α, [☀α]; &shr{α} (cell ty)) → ty).
+    typed_val (cell_get ty) (fn(∀ α, [α]; &shr{α} (cell ty)) → ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -146,7 +146,7 @@ Section typing.
       delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
 
   Lemma cell_replace_type ty :
-    typed_val (cell_replace ty) (fn(∀ α, [☀α]; &shr{α} cell ty, ty) → ty).
+    typed_val (cell_replace ty) (fn(∀ α, [α]; &shr{α} cell ty, ty) → ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>c x. simpl_subst.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index fedb4a378512c896faea3d4a87ec04b211ce52ad..0d18dc23ef8685b56d48901aaf4f1a150e23de7d 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,9 +11,8 @@ Section fake_shared_box.
 
   Lemma cell_replace_type ty :
     typed_val fake_shared_box
-      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
-          (fun '(α, β) => [# &shr{α}(&shr{β} ty)]%T)
-          (fun '(α, β) => &shr{α}box ty)%T).
+      (fn (fun '(α, β) => FP [# &shr{α}(&shr{β} ty)]
+                             (&shr{α}box ty) [α; β; α ⊑ β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 279a0e79457bce404b93ac7a83eb93a0e42677c9..10e930a39231a85d2f813aa7aec005decd8d81c4 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -19,7 +19,7 @@ Section option.
 
   Lemma option_as_mut_type Ï„ :
     typed_val
-      option_as_mut (fn(∀ α, [☀α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
+      option_as_mut (fn(∀ α, [α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
       inv_vec p=>o. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index e90a045f250d01995554137f37aff10d854d6aec..fd406c49bdaf3f6c547b010fda2c720560373cbd 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -56,8 +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 '(α, β) => [☀α; ☀β])%EL (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
-                                       (fun '(α, β) => ref β ty)%T).
+      (fn (fun '(α, β) => FP [# &shr{α}(ref β ty)]%T (ref β ty)%T [α; β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -117,9 +116,7 @@ Section ref_functions.
 
   Lemma ref_deref_type ty :
     typed_val ref_deref
-      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
-          (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
-          (fun '(α, β) => &shr{α}ty)%T).
+      (fn (fun '(α, β) => FP [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T [α; β; α ⊑ β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -156,7 +153,7 @@ Section ref_functions.
       let: "r" := new [ #0] in "return" ["r"].
 
   Lemma ref_drop_type ty :
-    typed_val ref_drop (fn(∀ α, [☀α]; ref α ty) → unit).
+    typed_val ref_drop (fn(∀ α, [α]; ref α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -221,7 +218,8 @@ Section ref_functions.
 
   Lemma ref_map_type ty1 ty2 envty E :
     typed_val ref_map
-      (fn(∀ β, [☀β] ++ E; ref β ty1, fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
+      (fn(∀ β, [β]%EL ++ E;
+            ref β ty1, fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
        → ref β ty2).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
@@ -240,9 +238,9 @@ Section ref_functions.
     iDestruct "HE" as "[HE HE']". iDestruct "Hν" as "[Hν Hν']".
     remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
     iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
-    iApply (type_type ((☀ (α ⊓ ν)) :: E)%EL []
+    iApply (type_type ((α ⊓ ν) :: E)%EL []
         [k ◁cont([], λ _:vec val 0, [ #lref ◁ own_ptr 2 (&shr{α ⊓ ν}ty2)])]%CC
-        [ f ◁ box (fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
+        [ f ◁ box (fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
           #lref ◁ own_ptr 2 (&shr{α ⊓ ν}ty1); env ◁ box envty ]%TC
        with "[] LFT Hna [HE Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 706404bdedbfadd2cf55e48902ccb576985633c4..f5e4931519f6d41333b7e0cb38a90c9037609a92 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -20,8 +20,7 @@ Section refcell_functions.
        delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
 
   Lemma refcell_new_type ty :
-    typed_val (refcell_new ty)
-      (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
+    typed_val (refcell_new ty) (fn([]; ty) → refcell ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -58,8 +57,7 @@ Section refcell_functions.
        delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
 
   Lemma refcell_into_inner_type ty :
-    typed_val (refcell_into_inner ty)
-                   (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
+    typed_val (refcell_into_inner ty) (fn([]; refcell ty) → ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -93,8 +91,7 @@ Section refcell_functions.
       "return" ["x"].
 
   Lemma refcell_get_mut_type ty :
-    typed_val refcell_get_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
+    typed_val refcell_get_mut (fn(∀ α, [α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -143,8 +140,7 @@ Section refcell_functions.
         delete [ #1; "x"];; "return" ["r"].
 
   Lemma refcell_try_borrow_type ty :
-    typed_val refcell_try_borrow
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (ref α ty))%T).
+    typed_val refcell_try_borrow (fn(∀ α, [α] ; &shr{α}(refcell ty)) → option (ref α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -249,7 +245,7 @@ Section refcell_functions.
 
   Lemma refcell_try_borrow_mut_type ty :
     typed_val refcell_try_borrow_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (refmut α ty))%T).
+              (fn(∀ α, [α]; &shr{α}(refcell ty)) → option (refmut α 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 d410c343f2fbc2f56b4b491d98e5e8f5049ee5c3..07088ab1e6ef453783c877469d3c7cbd1c452f1c 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -20,9 +20,7 @@ Section refmut_functions.
 
   Lemma refmut_deref_type ty :
     typed_val refmut_deref
-      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
-          (fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
-          (fun '(α, β) => &shr{α}ty)%T).
+      (fn (fun '(α, β) => FP [# &shr{α}(refmut β ty)]%T (&shr{α}ty) [α; β; α ⊑ β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -62,9 +60,8 @@ Section refmut_functions.
 
   Lemma refmut_derefmut_type ty :
     typed_val refmut_derefmut
-      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
-          (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
-          (fun '(α, β) => &uniq{α}ty)%T).
+      (fn (fun '(α, β) => FP [# &uniq{α}(refmut β ty)]%T
+                             (&uniq{α}ty)%T [α; β; α ⊑ β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -117,7 +114,7 @@ Section refmut_functions.
       let: "r" := new [ #0] in "return" ["r"].
 
   Lemma refmut_drop_type ty :
-    typed_val refmut_drop (fn(∀ α, [☀α]; refmut α ty) → unit).
+    typed_val refmut_drop (fn(∀ α, [α]; refmut α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -171,9 +168,9 @@ Section refmut_functions.
 
   Lemma refmut_map_type ty1 ty2 envty E :
     typed_val refmut_map
-      (fn(∀ β, [☀β] ++ E; refmut β ty1,
-                          fn(∀ α, [☀α] ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
-                          envty)
+      (fn(∀ β, [β]%EL ++ E; refmut β ty1,
+                         fn(∀ α, [α]%EL ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
+                         envty)
        → refmut β ty2).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -193,9 +190,9 @@ Section refmut_functions.
     iDestruct "HE" as "[HE HE']". iDestruct "Hν" as "[Hν Hν']".
     remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
     iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
-    iApply (type_type ((☀ (α ⊓ ν)) :: E)%EL []
+    iApply (type_type ((α ⊓ ν) :: E)%EL []
         [k ◁cont([], λ _:vec val 0, [ #lref ◁ own_ptr 2 (&uniq{α ⊓ ν}ty2)])]%CC
-        [ f ◁ box (fn(∀ α, [☀α] ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2);
+        [ f ◁ box (fn(∀ α, [α]%EL ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2);
           #lref ◁ own_ptr 2 (&uniq{α ⊓ ν}ty1); env ◁ box envty ]%TC
        with "[] LFT Hna [HE Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index cd4dc556e972031b4bf48de9d17704a4cc0a392d..2a6caa17c1cfb08d21ca1a7ca236e7b5aa2368a5 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -20,7 +20,7 @@ Section rwlock_functions.
        delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
 
   Lemma rwlock_new_type ty :
-    typed_val (rwlock_new ty) (fn (λ _, []) (λ _, [# ty]) (λ _:(), rwlock ty)).
+    typed_val (rwlock_new ty) (fn([]; ty) → rwlock ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -56,8 +56,7 @@ Section rwlock_functions.
        delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
 
   Lemma rwlock_into_inner_type ty :
-    typed_val (rwlock_into_inner ty)
-        (fn (λ _, []) (λ _, [# rwlock ty]) (λ _:(), ty)).
+    typed_val (rwlock_into_inner ty) (fn([] ; rwlock ty) → ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -91,8 +90,7 @@ Section rwlock_functions.
       "return" ["x"].
 
   Lemma rwlock_get_mut_type ty :
-    typed_val rwlock_get_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (rwlock ty)])%T (λ α, &uniq{α} ty)%T).
+    typed_val rwlock_get_mut (fn(∀ α, [α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -141,8 +139,7 @@ Section rwlock_functions.
 
   Lemma rwlock_try_read_type ty :
     typed_val rwlock_try_read
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
-            (λ α, option (rwlockreadguard α ty))%T).
+        (fn(∀ α, [α]; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -257,8 +254,7 @@ Section rwlock_functions.
 
   Lemma rwlock_try_write_type ty :
     typed_val rwlock_try_write
-        (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
-            (λ α, option (rwlockwriteguard α ty))%T).
+        (fn(∀ α, [α]; &shr{α}(rwlock ty)) → option (rwlockwriteguard α 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/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 12ececef0f687202b63dbe1847280ad196c85e24..d76e2b77fcbe14cf45e64b603c08902c73ebf536 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,9 +20,8 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_deref_type ty :
     typed_val rwlockreadguard_deref
-      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
-          (fun '(α, β) => [# &shr{α}(rwlockreadguard β ty)]%T)
-          (fun '(α, β) => &shr{α}ty)%T).
+      (fn (fun '(α, β) => FP [# &shr{α}(rwlockreadguard β ty)]
+                             (&shr{α}ty) [α; β; α ⊑ β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -62,7 +61,7 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_drop_type ty :
     typed_val rwlockreadguard_drop
-                   (fn(∀ α, [☀α]; rwlockreadguard α ty) → unit).
+              (fn(∀ α, [α]; rwlockreadguard α ty) → unit).
   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 72a7e3272bbc49a72c041c0a84cea4e7935aaf90..3e3d4ee0bbfc70551ea9a3af8f7926c796dd4348 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,9 +20,9 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_deref_type ty :
     typed_val rwlockwriteguard_deref
-      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
-          (fun '(α, β) => [# &shr{α}(rwlockwriteguard β ty)]%T)
-          (fun '(α, β) => &shr{α}ty)%T).
+      (fn (fun '(α, β) => FP [# &shr{α}(rwlockwriteguard β ty)]
+                             (&shr{α}ty)
+                             [α; β; α ⊑ β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -63,9 +63,9 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_derefmut_type ty :
     typed_val rwlockwriteguard_derefmut
-      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
-          (fun '(α, β) => [# &uniq{α}(rwlockwriteguard β ty)]%T)
-          (fun '(α, β) => &uniq{α}ty)%T).
+      (fn (fun '(α, β) => FP [# &uniq{α}(rwlockwriteguard β ty)]
+                             (&uniq{α}ty)
+                             [α; β; α ⊑ β]%EL)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -111,7 +111,7 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_drop_type ty :
     typed_val rwlockwriteguard_drop
-                   (fn(∀ α, [☀α]; rwlockwriteguard α ty) → unit).
+              (fn(∀ α, [α]; rwlockwriteguard α ty) → unit).
   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 0874f490422c4842c03562cfa9653c7b1062bf27..45cf25e5bbddca11c8f96277a1a7ce20cb890fc1 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -84,8 +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]
-              (λ _, [# 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]").