also show wp_app for lists

theories/lang/derived.v

@@ -44,7 +44,7 @@ Proof.
     rewrite big_sepL_cons. iFrame.
 Qed.
 
-Lemma wp_app {n} (Q : nat → val → iProp Σ) E f (el : vec expr n) Φ :
+Lemma wp_app_vec {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) -∗
@@ -54,6 +54,19 @@ Proof.
   iIntros (Hf). iApply (wp_app_ind _ _ _ _ []). done.
 Qed.
 
+Lemma wp_app (Q : nat → val → iProp Σ) E f el Φ :
+  is_Some (to_val f) →
+  ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
+    (∀ vl : list val, ⌜length vl = length el⌝ -∗ ([∗ list] k ↦ v ∈ vl, Q k v) -∗
+                    WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+    WP App f el @ E {{ Φ }}.
+Proof.
+  iIntros (Hf) "Hel HΦ". rewrite -(vec_to_list_of_list el).
+  iApply (wp_app_vec with "* Hel"); first done.
+  iIntros (vl). iApply ("HΦ" $! (vec_to_list vl)).
+  rewrite vec_to_list_length vec_to_list_of_list. done.
+Qed.
+
 (** Proof rules for the sugar *)
 Lemma wp_lam E xl e e' el Φ :
   Forall (λ ei, is_Some (to_val ei)) el →

theories/typing/function.v

@@ -102,7 +102,7 @@ Section fn.
     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. rewrite -vec_to_list_cons.
-    iApply (wp_app (λ i v, match i with O => ⌜v = k⌝ ∗ _ | S i =>
+    iApply (wp_app_vec (λ 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.