diff --git a/theories/lecture_notes/lists.v b/theories/lecture_notes/lists.v
index d93426679ff3120e8a34c42a1fac6d9845536486..b8138ef395b69b837394691adbe3dbb16fceb7fb 100644
--- a/theories/lecture_notes/lists.v
+++ b/theories/lecture_notes/lists.v
@@ -385,31 +385,30 @@ Proof.
 Qed.
 
 
-Lemma filter_spec (hd p : val) (xs : list val) (P : val -> bool) :
+Lemma filter_spec (hd p : val) (xs : list val) (R : val -> bool) (Q : val → iProp Σ) :
   {{{ is_list hd xs
       ∗ (∀ x : val ,
-           {{{ True }}}
+           {{{ Q x }}}
            p x
-           {{{r, RET r; ⌜r = #(P x)⌝ }}})
+           {{{r, RET r; ⌜r = #(R x)⌝ }}}) ∗ [∗ list] x ∈ xs, Q x
   }}}
   filter p hd
   {{{ v, RET v; is_list hd xs
-                ∗ is_list v (List.filter P xs)
+                ∗ is_list v (List.filter R xs)
   }}}.
 Proof.
-  iIntros (Ï•) "[H_isList #H_p] H_Ï•". wp_rec. wp_pures.
-  iApply (foldr_spec_PI (fun x => True)%I
-                        (fun xs' acc => is_list acc (List.filter P xs'))%I
-                  with "[$H_isList] [H_Ï•]").
-  - iSplitL.
-    + iIntros (x a' ?) "!# %Ï•'". iIntros "[_ H_isList] H_Ï•'".
-      repeat (wp_pure _). wp_bind (p x). iApply "H_p"; first done.
-      iNext. iIntros (r) "H". iSimplifyEq. destruct (P x); wp_if.
+  iIntros (Ï•) "(H_isList & #H_p & HQs) H_Ï•". wp_rec. wp_pures.
+  iApply (foldr_spec_PI Q
+                        (fun xs' acc => is_list acc (List.filter R xs'))%I
+                  with "[$H_isList HQs] [H_Ï•]").
+  - iSplitR.
+    + iIntros (x a' ?) "!# %Ï•'". iIntros "[HQ H_isList] H_Ï•'".
+      repeat (wp_pure _). wp_bind (p x). iApply ("H_p" with "[$HQ]").
+      iNext. iIntros (r) "H". iSimplifyEq. destruct (R x); wp_if.
       * wp_rec. wp_pures. wp_alloc l. wp_pures. iApply "H_Ï•'".
         iExists l, a'. by iFrame.
       * by iApply "H_Ï•'".
-    + iSplit; last done.
-      rewrite big_sepL_forall. eauto.
+    + by iSplit.
   - iNext. iApply "H_Ï•".
 Qed.