diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 3e7332785d486c5bec1fd5b921ba033bea8f1e71..05c665b19ee35cf23a400b4068a245226e6b8384 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -159,18 +159,17 @@ Definition subst' (mx : binder) (es : expr) : expr → expr :=
 Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :=
   match xl, esl with
   | [], [] => Some e
-  | x::xl, es::esl => subst_l xl esl (subst' x es e)
+  | x::xl, es::esl => subst' x es <$> subst_l xl esl e
   | _, _ => None
   end.
 
-Definition subst_v (xl : list binder) (esl : vec expr (length xl))
+Definition subst_v (xl : list binder) (vsl : vec val (length xl))
                    (e : expr) : expr :=
-  from_option id (Var "" (* Dummy *)) (subst_l xl esl e).
-Lemma subst_v_eq (xl : list binder) (esl : vec expr (length xl)) e :
-  Some $ subst_v xl esl e = subst_l xl esl e.
+  Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
+Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
+  Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
 Proof.
-  unfold subst_v. destruct subst_l eqn:EQ; first done. exfalso. revert esl e EQ.
-  induction xl=>/= esl; inv_vec esl; first done. simpl. eauto.
+  revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
 Qed.
 
 (** The stepping relation *)
@@ -230,8 +229,8 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
 | BetaS f xl e e' el σ:
     Forall (λ ei, is_Some (to_val ei)) el →
     Closed (f :b: xl +b+ []) e →
-    subst_l xl el e = Some e' →
-    head_step (App (Rec f xl e) el) σ (subst' f (Rec f xl e) e') σ []
+    subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
+    head_step (App (Rec f xl e) el) σ e' σ []
 | ReadScS l n v σ:
     σ !! l = Some (RSt n, v) →
     head_step (Read ScOrd (Lit $ LitLoc l)) σ (of_val v) σ []
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 5810abc7d80fc38dd57ca961c3c6fc257e225e6c..f0c96434453723966dd908574f62adf9c8641f33 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -146,9 +146,8 @@ Lemma wp_rec E e f xl erec erec' el Φ :
   e = Rec f xl erec → (* to avoids recursive calls being unfolded *)
   Forall (λ ei, is_Some (to_val ei)) el →
   Closed (f :b: xl +b+ []) erec →
-  subst_l xl el erec = Some erec' →
-  ▷ WP subst' f e erec' @ E {{ Φ }} -∗
-  WP App e el @ E {{ Φ }}.
+  subst_l (f::xl) (e::el) erec = Some erec' →
+  ▷ WP erec' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
 Proof.
   iIntros (-> ???) "?". iApply ownP_lift_pure_det_head_step; subst; eauto.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index b5a608107b471e2c68a930c33212a7845d39a0e7..515c2dd4af4090f6bbff2da232c620a12f651e90 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -22,7 +22,7 @@ Section typing.
   Lemma type_cont E L1 L2 C T argsb econt e2 T' kb :
     Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
     (∀ k args, typed_body E L1 (CCtx_iscont k L1 _ T' :: C) (T' args)
-                          (subst' kb k $ subst_v argsb (vmap of_val args) econt)) →
+                          (subst_v (kb::argsb) (k:::args) econt)) →
     (∀ k, typed_body E L2 (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) →
     typed_body E L2 C T (let: kb := Rec kb argsb econt in e2).
   Proof.
@@ -33,7 +33,7 @@ Section typing.
     iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *").
     iIntros (args) "Htl HL HT". iApply wp_rec; try done.
     { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
-    { by rewrite -vec_to_list_map -subst_v_eq. }
+    { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
     (* FIXME: iNext here unfolds things in the context. *)
     iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
     by iApply "IH".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 76c6fe6beb5f82adaf626d1cb5421cbc076924c0..abd45a4eaf2b7c110f8a4c5622e35245ca2a5377 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -12,13 +12,15 @@ Section fn.
 
   Program Definition fn {A n} (E : A → elctx)
           (tys : A → vec type n) (ty : A → type) : type :=
-    {| st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ □ ∀ (x : A) (args : vec val n) (k : val),
-         typed_body (E x) []
-                    [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
-                    (zip_with (TCtx_hasty ∘ of_val) args (tys x))
-                    (f (of_val <$> (k :: args : list val))))%I |}.
+    {| 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) []
+                       [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
+                       (zip_with (TCtx_hasty ∘ of_val) xl (tys x))
+                       (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
   Next Obligation.
-    iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
+    iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
   Qed.
 
   Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty).
@@ -34,12 +36,13 @@ Section typing.
     subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
   Proof.
     intros Htys Hty. apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
-    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE HL HC HT".
+    iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iAlways. iNext.
+    rewrite /typed_body. iIntros "* #HEAP _ Htl HE HL HC HT".
     iDestruct (elctx_interp_persist with "HE") as "#HE'".
     iApply ("Hf" with "* HEAP LFT Htl HE HL [HC] [HT]").
-    - iIntros "HE". unfold cctx_interp. iIntros (e) "He".
-      iDestruct "He" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
+    - iIntros "HE". unfold cctx_interp. iIntros (elt) "Helt".
+      iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
       iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
       iApply ("HC" $! (CCtx_iscont _ _ _ _) with "[%] * Htl HL >").
       {  by apply elem_of_list_singleton. }
@@ -68,8 +71,9 @@ Section typing.
     subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
   Proof.
     apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT _ _ Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
-    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# *". iApply "Hf".
+    iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
+    rewrite /typed_body. iAlways. iNext. iIntros "*". iApply "Hf".
   Qed.
 
   Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
@@ -77,8 +81,9 @@ Section typing.
     subtype E0 L0 (fn E' tys ty) (fn E tys ty).
   Proof.
     intros HEE'. apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT _ _ Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
-    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE #HL HC HT".
+    iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. rewrite /typed_body.
+    iAlways. iNext. iIntros "* #HEAP _ Htl HE #HL HC HT".
     iMod (HEE' x with "[%] HE HL") as (qE') "[HE Hclose]". done.
     iApply ("Hf" with "* HEAP LFT Htl HE HL [Hclose HC] HT"). iIntros "HE".
     iApply fupd_cctx_interp. iApply ("HC" with ">").
@@ -90,8 +95,9 @@ Section typing.
     subtype E0 L0 (fn (λ x, ELCtx_Incl κ κ' :: E x) tys ty) (fn E tys ty).
   Proof.
     intros Hκκ'. apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
-    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE #HL HC HT".
+    iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. rewrite /typed_body.
+    iAlways. iNext. iIntros "* #HEAP _ Htl HE #HL HC HT".
     iApply ("Hf" with "* HEAP LFT Htl [HE] HL [HC] HT").
     { rewrite /elctx_interp big_sepL_cons. iFrame. iApply (Hκκ' with "HE0 HL0"). }
     rewrite /elctx_interp big_sepL_cons. iIntros "[_ HE]". by iApply "HC".
@@ -118,9 +124,14 @@ Section typing.
               (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
       iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
       iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
-    - simpl. iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
-      iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (f) "[EQ #Hf]".
-      iDestruct "EQ" as %[=->]. iSpecialize ("Hf" $! x vl k).
+    - 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.
+      { 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).
       iMod (HEsat with "[%] HE HL") as (q') "[HE' Hclose]"; first done.
       iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT']").
       + by rewrite /llctx_interp big_sepL_nil.
@@ -128,8 +139,8 @@ Section typing.
         iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
         iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ HT".
         iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
-        iApply ("HC" $! args with "Htl HL"). rewrite tctx_interp_singleton tctx_interp_cons.
-        iFrame.
+        iApply ("HC" $! args with "Htl HL").
+        rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
       + rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
                 (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
         iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
@@ -139,23 +150,21 @@ Section typing.
         (tys : A → vec type (length argsb)) ty
         T `{!CopyC T, !SendC T} :
     Closed (fb :b: kb :b: argsb +b+ []) e →
-    (∀ x f k (args : vec val _),
+    (∀ x (f : val) k (args : vec val _),
         typed_body (E' x) [] [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
                    (TCtx_hasty f (fn E' tys ty) ::
                       zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
-                   (subst' fb f $ subst_v (kb :: argsb) (vmap of_val $ k ::: args) e)) →
+                   (subst_v (fb :: kb :: argsb) (f ::: k ::: args) e)) →
     typed_instruction_ty E L T (Rec fb (kb :: argsb) e) (fn E' tys ty).
   Proof.
     iIntros (Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite decide_left. done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
-    iExists _. iSplit; first done. iAlways. clear qE.
-    iIntros (x args k tid' qE) "_ _ Htl HE HL HC HT'". iApply wp_rec; try done.
-    { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
-    { by rewrite -vec_to_list_cons -vec_to_list_map -subst_v_eq. }
+    iExists fb, kb, argsb, e, _. iSplit. done. iSplit. done. iAlways. iNext. clear qE.
+    iIntros (x k args tid' qE) "_ _ Htl HE HL HC HT'".
     iApply (Hbody with "* HEAP LFT Htl HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
-    iApply sendc_change_tid. by iNext.
+    by iApply sendc_change_tid.
   Qed.
 End typing.