diff --git a/opam.pins b/opam.pins
index c51c3e1b26c6a0b11fe328d482c1c3d55246f71d..90d82d5a4825aa26ed7317a194b7da14330b597b 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1c9e858188578a65bf014ed8a8a9404f87054848
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e2b843075894275afd52c19c83e4f5f812afdbab
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 40ea3607e6ae1b44ab4e13e89d023b12380828bb..dbf09fff90a0e2d1984b2e2c593125ac02052032 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -22,27 +22,36 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 
 (** Proof rules for working on the n-ary argument list. *)
-Lemma wp_app (P : expr → iProp Σ) (Q : val → iProp Σ) E f el Φ :
+Lemma wp_app_ind {n} (Q : nat → val → iProp Σ) E f (el : vec expr n) (vs : list val) Φ :
   is_Some (to_val f) →
-  ([∗ list] e ∈ el, P e) -∗ □ (∀ e, P e -∗ WP e @ E {{ Q }}) -∗
-    (∀ vl, ([∗ list] v ∈ vl, Q v) -∗ WP App f (of_val <$> vl) @ E {{ Φ }}) -∗
-    WP App f el @ E {{ Φ }}.
+   ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
+   (∀ vl : vec val n, ([∗ list] k ↦ v ∈ vl, Q k v) -∗
+                    WP App f (map of_val (vs ++ vl)) @ E {{ Φ }}) -∗
+    WP App f (map of_val vs ++ el) @ E {{ Φ }}.
 Proof.
-  iIntros (Hf) "Hel #HPQ HΦ".
-  assert (el = ((of_val <$> ([] : list val)) ++ el)) as -> by reflexivity.
-  rewrite big_sepL_app. iDestruct "Hel" as "[Hvl Hel]".
-  iAssert ([∗ list] y ∈ [], Q y)%I with "[Hvl]" as "Hvl".
-  { by rewrite big_sepL_nil. }
-  remember [] as vl. clear Heqvl. iInduction el as [|e el] "IH" forall (vl).
-  - rewrite app_nil_r. by iApply "HΦ".
-  - destruct Hf as [vf Hf]. set (K := AppRCtx vf vl el).
-    rewrite (_ : App f ((of_val <$> vl) ++ e :: el) = fill_item K e); last first.
+  iIntros (Hf) "Hel HΦ". iInduction el as [|e n el] "IH" forall (vs Q).
+  - iSpecialize ("HΦ" $! [#]). rewrite !app_nil_r. iApply "HΦ".
+    by rewrite !big_sepL_nil.
+  - destruct Hf as [vf Hf]. set (K := AppRCtx vf vs el).
+    rewrite (_ : App f ((map of_val vs) ++ e ::: el) = fill_item K e); last first.
     { simpl. f_equal. by erewrite of_to_val. }
-    iApply wp_bindi. rewrite big_sepL_cons. iDestruct "Hel" as "[He Hel]".
-    iApply (wp_wand with "[He]"); first by iApply "HPQ". iIntros (v) "HQ".
-    simpl. erewrite of_to_val by done. iSpecialize ("IH" $! (vl ++ [v])).
-    rewrite [of_val <$> vl ++ [v]]map_app /= -app_assoc /=. iApply ("IH" with "Hel HΦ").
-    rewrite big_sepL_app big_sepL_singleton. iFrame.
+    iApply wp_bindi. rewrite vec_to_list_cons big_sepL_cons. iDestruct "Hel" as "[He Hel]".
+    iApply (wp_wand with "He"). iIntros (v) "HQ".
+    simpl. erewrite of_to_val by done. iSpecialize ("IH" $! (vs ++ [v])).
+    rewrite [map of_val (vs ++ [#v])]map_app /= -app_assoc /=.
+    iApply ("IH" with "Hel"). iIntros (vl) "Hvl".
+    iSpecialize ("HΦ" $! (v ::: vl)). rewrite -app_assoc /=. iApply "HΦ".
+    rewrite big_sepL_cons. iFrame.
+Qed.
+
+Lemma wp_app {n} (Q : nat → val → iProp Σ) E f (el : vec expr n) Φ :
+  is_Some (to_val f) →
+  ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
+    (∀ vl : vec val n, ([∗ list] k ↦ v ∈ vl, Q k v) -∗
+                    WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+    WP App f el @ E {{ Φ }}.
+Proof.
+  iIntros (Hf). iApply (wp_app_ind _ _ _ _ []). done.
 Qed.
 
 (** Proof rules for the sugar *)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7d8e766ce774420dd33094779df743e68c3499bc..33a480efde03f0b73a5d7f2adb0d057851b382cf 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -101,11 +101,27 @@ Section fn.
     rewrite tctx_interp_cons. iIntros "[Hf HT]".
     wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "[% Hf]".
     iMod (HTsat with "LFT HE HL HT") as "(HE & HL & HT)". rewrite tctx_interp_app.
-    iDestruct "HT" as "[Hargs HT']". clear HTsat.
-    (* TODO: I have no idea how to reduce all the ps properly to their values. This induction is probably not right, but at least it checks the case of the empty list. *)
-    iInduction ps as [|p' n ps] "IH" forall (tys).
-    - iDestruct "Hf" as (f) "[EQ #Hf]". iDestruct "EQ" as %[=->].
-      iSpecialize ("Hf" $! x [#] k). simpl.
+    iDestruct "HT" as "[Hargs HT']". clear HTsat. rewrite -vec_to_list_cons.
+    iApply (wp_app (λ i v, match i with O => ⌜v = k⌝ ∗ _ | S i =>
+                           ∀ ty, ⌜(tys x : list type) !! i = Some ty⌝ →
+                                 tctx_elt_interp tid (TCtx_hasty v ty) end)%I
+            with "* [Hargs HC]"); first wp_done.
+    - rewrite big_sepL_cons. iSplitR "Hargs".
+      { iApply wp_value'. iSplit; first done. iApply "HC". }
+      clear dependent ty k p.
+      rewrite /tctx_interp. rewrite big_sepL_zip_with. iApply (big_sepL_mono with "Hargs").
+      simpl. iIntros (i p Hp) "HT". assert (Hlen := lookup_lt_Some _ _ _ Hp).
+      edestruct (lookup_lt_is_Some_2 (tys x)) as [ty Hty].
+      { move: Hlen. rewrite !vec_to_list_length. done. }
+      iSpecialize ("HT" with "* []"); first done.
+      iApply (wp_hasty with "HT"). iIntros (v') "[% Hown]". iIntros (ty') "#EQ".
+      rewrite Hty. iDestruct "EQ" as %[=<-]. iExists v'. iFrame "Hown".
+      iPureIntro. exact: eval_path_of_val.
+    - iIntros (vl'). assert (Hvl := Vector.eta vl'). remember (Vector.hd vl') as kv.
+      remember (Vector.tl vl') as vl. rewrite Hvl. simpl in *. clear dependent vl'.
+      rewrite big_sepL_cons. iIntros "[[% HC] Hvl]". subst kv.
+      iDestruct "Hf" as (f) "[EQ #Hf]". iDestruct "EQ" as %[=->].
+      iSpecialize ("Hf" $! x vl k). 
       iMod (HEsat with "[%] HE HL") as (q') "[HE' Hclose]"; first done.
       iApply ("Hf" with "LFT HE' [] [HC Hclose HT']").
       + by rewrite /llctx_interp big_sepL_nil.
@@ -115,9 +131,8 @@ Section fn.
         iIntros (args) "_ HT". iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
         iApply ("HC" $! args with "HL"). rewrite tctx_interp_singleton tctx_interp_cons.
         iFrame.
-      + done.
-    - (* TODO: The IH is not usable here. What we really want is to do induction over "how many of the arguments still need to be evaluated", so the base case has all the ps evaluated and the inductive case evaluates one of them. *)
-  Abort.
+      + rewrite /tctx_interp big_sepL_zip_with. done.
+  Qed.
 
   Lemma typed_fn {A n m} E L E' (tys : A → vec type n) ty fb kb (argsb : vec binder n) ef e
        (cps : vec path m) (ctyl : vec type m) `{!LstCopy ctyl, !LstSend ctyl} :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 225d245710c84c85b997ce96ec3c6c166fbd13e8..67e025dda6ee4e71291e4bc65fb56106ab0113bc 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -20,6 +20,10 @@ Section type_context.
     | e => to_val e
     end.
 
+  Lemma eval_path_of_val (v : val) :
+    eval_path v = Some v.
+  Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
+
   (* TODO: Consider mking this a pair of a path and the rest. We could
      then e.g. formulate tctx_elt_hasty_path more generally. *)
   Inductive tctx_elt : Type :=
@@ -35,6 +39,7 @@ Section type_context.
     end%I.
   (* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
   Global Arguments tctx_elt_interp : simpl never.
+
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.