diff --git a/stdpp/list_basics.v b/stdpp/list_basics.v
index 90a7410a2cb8070f9b35a0fd4496214fdd5d05a2..47f97b40dc7aaa80b3ecbdb1ee3f30977e79c16a 100644
--- a/stdpp/list_basics.v
+++ b/stdpp/list_basics.v
@@ -106,16 +106,6 @@ Global Instance list_filter {A} : Filter A (list A) :=
   | x :: l => if decide (P x) then x :: filter P l else filter P l
   end.
 
-(** The function [list_find P l] returns the first index [i] whose element
-satisfies the predicate [P]. *)
-Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A) :=
-  fix go l :=
-  match l with
-  | [] => None
-  | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
-  end.
-Global Instance: Params (@list_find) 3 := {}.
-
 (** The function [replicate n x] generates a list with length [n] of elements
 with value [x]. *)
 Fixpoint replicate {A} (n : nat) (x : A) : list A :=
diff --git a/stdpp/list_misc.v b/stdpp/list_misc.v
index d90721ba329b3fb71f1baf6035f9607bb6708914..b844f0b7e7cf65d0737eb653122a0c5f241170d6 100644
--- a/stdpp/list_misc.v
+++ b/stdpp/list_misc.v
@@ -2,6 +2,16 @@ From Coq Require Export Permutation.
 From stdpp Require Export numbers base option list_basics list_relations list_monad.
 From stdpp Require Import options.
 
+(** The function [list_find P l] returns the first index [i] whose element
+satisfies the predicate [P]. *)
+Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A) :=
+  fix go l :=
+  match l with
+  | [] => None
+  | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
+  end.
+Global Instance: Params (@list_find) 3 := {}.
+
 (** The function [resize n y l] takes the first [n] elements of [l] in case
 [length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
 a list of length [n]. *)
@@ -93,6 +103,140 @@ Context {A : Type}.
 Implicit Types x y z : A.
 Implicit Types l k : list A.
 
+(** * Properties of the [find] function *)
+Section find.
+  Context (P : A → Prop) `{!∀ x, Decision (P x)}.
+
+  Lemma list_find_Some l i x  :
+    list_find P l = Some (i,x) ↔
+      l !! i = Some x ∧ P x ∧ ∀ j y, l !! j = Some y → j < i → ¬P y.
+  Proof.
+    revert i. induction l as [|y l IH]; intros i; csimpl; [naive_solver|].
+    case_decide.
+    - split; [naive_solver lia|]. intros (Hi&HP&Hlt).
+      destruct i as [|i]; simplify_eq/=; [done|].
+      destruct (Hlt 0 y); naive_solver lia.
+    - split.
+      + intros ([i' x']&Hl&?)%fmap_Some; simplify_eq/=.
+        apply IH in Hl as (?&?&Hlt). split_and!; [done..|].
+        intros [|j] ?; naive_solver lia.
+      + intros (?&?&Hlt). destruct i as [|i]; simplify_eq/=; [done|].
+        rewrite (proj2 (IH i)); [done|]. split_and!; [done..|].
+        intros j z ???. destruct (Hlt (S j) z); naive_solver lia.
+  Qed.
+
+  Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
+  Proof.
+    induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
+    by destruct IH as [[i x'] ->]; [|exists (S i, x')].
+  Qed.
+
+  Lemma list_find_None l :
+    list_find P l = None ↔ Forall (λ x, ¬P x) l.
+  Proof.
+    rewrite eq_None_not_Some, Forall_forall. split.
+    - intros Hl x Hx HP. destruct Hl. eauto using list_find_elem_of.
+    - intros HP [[i x] (?%elem_of_list_lookup_2&?&?)%list_find_Some]; naive_solver.
+  Qed.
+
+  Lemma list_find_app_None l1 l2 :
+    list_find P (l1 ++ l2) = None ↔ list_find P l1 = None ∧ list_find P l2 = None.
+  Proof. by rewrite !list_find_None, Forall_app. Qed.
+
+  Lemma list_find_app_Some l1 l2 i x :
+    list_find P (l1 ++ l2) = Some (i,x) ↔
+      list_find P l1 = Some (i,x) ∨
+      length l1 ≤ i ∧ list_find P l1 = None ∧ list_find P l2 = Some (i - length l1,x).
+  Proof.
+    split.
+    - intros ([?|[??]]%lookup_app_Some&?&Hleast)%list_find_Some.
+      + left. apply list_find_Some; eauto using lookup_app_l_Some.
+      + right. split; [lia|]. split.
+        { apply list_find_None, Forall_lookup. intros j z ??.
+          assert (j < length l1) by eauto using lookup_lt_Some.
+          naive_solver eauto using lookup_app_l_Some with lia. }
+        apply list_find_Some. split_and!; [done..|].
+        intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
+        by rewrite lookup_app_r, Nat.add_sub' by lia.
+    - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
+      + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
+        assert (i < length l1) by eauto using lookup_lt_Some.
+        intros j y ?%lookup_app_Some; naive_solver eauto with lia.
+      + rewrite list_find_Some, lookup_app_Some. split_and!; [by auto..|].
+        intros j y [?|?]%lookup_app_Some ?; [|naive_solver auto with lia].
+        by eapply (Forall_lookup_1 (not ∘ P) l1); [by apply list_find_None|..].
+  Qed.
+  Lemma list_find_app_l l1 l2 i x:
+    list_find P l1 = Some (i, x) → list_find P (l1 ++ l2) = Some (i, x).
+  Proof. rewrite list_find_app_Some. auto. Qed.
+  Lemma list_find_app_r l1 l2:
+    list_find P l1 = None →
+    list_find P (l1 ++ l2) = prod_map (λ n, n + length l1) id <$> list_find P l2.
+  Proof.
+    intros. apply option_eq; intros [j y]. rewrite list_find_app_Some. split.
+    - intros [?|(?&?&->)]; naive_solver auto with f_equal lia.
+    - intros ([??]&->&?)%fmap_Some; naive_solver auto with f_equal lia.
+  Qed.
+
+  Lemma list_find_insert_Some l i j x y :
+    list_find P (<[i:=x]> l) = Some (j,y) ↔
+      (j < i ∧ list_find P l = Some (j,y)) ∨
+      (i = j ∧ x = y ∧ j < length l ∧ P x ∧ ∀ i' z, l !! i' = Some z → i' < i → ¬P z) ∨
+      (i < j ∧ ¬P x ∧ list_find P l = Some (j,y) ∧ ∀ z, l !! i = Some z → ¬P z) ∨
+      (∃ z, i < j ∧ ¬P x ∧ P y ∧ P z ∧ l !! i = Some z ∧ l !! j = Some y ∧
+            ∀ i' z, l !! i' = Some z → i' ≠ i → i' < j → ¬P z).
+   Proof.
+     split.
+     - intros ([(->&->&?)|[??]]%list_lookup_insert_Some&?&Hleast)%list_find_Some.
+       { right; left. split_and!; [done..|]. intros k z ??.
+         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
+       assert (j < i ∨ i < j) as [?|?] by lia.
+       { left. rewrite list_find_Some. split_and!; [by auto..|]. intros k z ??.
+         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
+       right; right. assert (j < length l) by eauto using lookup_lt_Some.
+       destruct (lookup_lt_is_Some_2 l i) as [z ?]; [lia|].
+       destruct (decide (P z)).
+       { right. exists z. split_and!; [done| |done..|].
+         + apply (Hleast i); [|done]. by rewrite list_lookup_insert by lia.
+         + intros k z' ???.
+           apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
+       left. split_and!; [done|..|naive_solver].
+       + apply (Hleast i); [|done]. by rewrite list_lookup_insert by lia.
+       + apply list_find_Some. split_and!; [by auto..|]. intros k z' ??.
+         destruct (decide (k = i)) as [->|]; [naive_solver|].
+         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia.
+     - intros [[? Hl]|[(->&->&?&?&Hleast)|[(?&?&Hl&Hnot)|(z&?&?&?&?&?&?&?Hleast)]]];
+         apply list_find_Some.
+       + apply list_find_Some in Hl as (?&?&Hleast).
+         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
+         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
+       + rewrite list_lookup_insert by done. split_and!; [by auto..|].
+         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
+       + apply list_find_Some in Hl as (?&?&Hleast).
+         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
+         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
+       + rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
+         intros k z' [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
+  Qed.
+
+  Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l :
+    (∀ x, P x ↔ Q x) →
+    list_find P l = list_find Q l.
+  Proof.
+    intros HPQ. induction l as [|x l IH]; simpl; [done|].
+    by rewrite (decide_ext (P x) (Q x)), IH by done.
+  Qed.
+End find.
+
+Lemma list_find_fmap {B} (f : A → B) (P : B → Prop)
+    `{!∀ y : B, Decision (P y)} (l : list A) :
+  list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
+Proof.
+  induction l as [|x l IH]; [done|]; csimpl. (* csimpl re-folds fmap *)
+  case_decide; [done|].
+  rewrite IH. by destruct (list_find (P ∘ f) l).
+Qed.
+
 (** ** Properties of the [resize] function *)
 Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
 Proof. revert n. induction l; intros [|?]; f_equal/=; auto. Qed.
diff --git a/stdpp/list_monad.v b/stdpp/list_monad.v
index 8090d9517a257768bece8f0f8f8a1ce1eea11a61..3d0c0defe42897141bbc9dfc26f4de5e55f102d9 100644
--- a/stdpp/list_monad.v
+++ b/stdpp/list_monad.v
@@ -227,13 +227,6 @@ Section fmap.
     intros ?%list_fmap_inj ?? ?%list_equiv_Forall2%(inj _).
     by apply list_equiv_Forall2.
   Qed.
-  Lemma list_find_fmap (P : B → Prop) `{∀ x, Decision (P x)} (l : list A) :
-    list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
-  Proof.
-    induction l as [|x l IH]; [done|]; csimpl. (* csimpl re-folds fmap *)
-    case_decide; [done|].
-    rewrite IH. by destruct (list_find (P ∘ f) l).
-  Qed.
 
   (** A version of [NoDup_fmap_2] that does not require [f] to be injective for
       *all* inputs. *)
diff --git a/stdpp/list_relations.v b/stdpp/list_relations.v
index 9ad236bb7744bd87feeadc6446b8644a1796ad42..be4e4b3896a89f8cf6ee76286d75087d7c13c51c 100644
--- a/stdpp/list_relations.v
+++ b/stdpp/list_relations.v
@@ -1904,131 +1904,6 @@ Section setoid.
   Qed.
 End setoid.
 
-(** * Properties of the [find] function *)
-Section find.
-  Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
-
-  Lemma list_find_Some l i x  :
-    list_find P l = Some (i,x) ↔
-      l !! i = Some x ∧ P x ∧ ∀ j y, l !! j = Some y → j < i → ¬P y.
-  Proof.
-    revert i. induction l as [|y l IH]; intros i; csimpl; [naive_solver|].
-    case_decide.
-    - split; [naive_solver lia|]. intros (Hi&HP&Hlt).
-      destruct i as [|i]; simplify_eq/=; [done|].
-      destruct (Hlt 0 y); naive_solver lia.
-    - split.
-      + intros ([i' x']&Hl&?)%fmap_Some; simplify_eq/=.
-        apply IH in Hl as (?&?&Hlt). split_and!; [done..|].
-        intros [|j] ?; naive_solver lia.
-      + intros (?&?&Hlt). destruct i as [|i]; simplify_eq/=; [done|].
-        rewrite (proj2 (IH i)); [done|]. split_and!; [done..|].
-        intros j z ???. destruct (Hlt (S j) z); naive_solver lia.
-  Qed.
-
-  Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
-  Proof.
-    induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
-    by destruct IH as [[i x'] ->]; [|exists (S i, x')].
-  Qed.
-
-  Lemma list_find_None l :
-    list_find P l = None ↔ Forall (λ x, ¬P x) l.
-  Proof.
-    rewrite eq_None_not_Some, Forall_forall. split.
-    - intros Hl x Hx HP. destruct Hl. eauto using list_find_elem_of.
-    - intros HP [[i x] (?%elem_of_list_lookup_2&?&?)%list_find_Some]; naive_solver.
-  Qed.
-
-  Lemma list_find_app_None l1 l2 :
-    list_find P (l1 ++ l2) = None ↔ list_find P l1 = None ∧ list_find P l2 = None.
-  Proof. by rewrite !list_find_None, Forall_app. Qed.
-
-  Lemma list_find_app_Some l1 l2 i x :
-    list_find P (l1 ++ l2) = Some (i,x) ↔
-      list_find P l1 = Some (i,x) ∨
-      length l1 ≤ i ∧ list_find P l1 = None ∧ list_find P l2 = Some (i - length l1,x).
-  Proof.
-    split.
-    - intros ([?|[??]]%lookup_app_Some&?&Hleast)%list_find_Some.
-      + left. apply list_find_Some; eauto using lookup_app_l_Some.
-      + right. split; [lia|]. split.
-        { apply list_find_None, Forall_lookup. intros j z ??.
-          assert (j < length l1) by eauto using lookup_lt_Some.
-          naive_solver eauto using lookup_app_l_Some with lia. }
-        apply list_find_Some. split_and!; [done..|].
-        intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
-        by rewrite lookup_app_r, Nat.add_sub' by lia.
-    - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
-      + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
-        assert (i < length l1) by eauto using lookup_lt_Some.
-        intros j y ?%lookup_app_Some; naive_solver eauto with lia.
-      + rewrite list_find_Some, lookup_app_Some. split_and!; [by auto..|].
-        intros j y [?|?]%lookup_app_Some ?; [|naive_solver auto with lia].
-        by eapply (Forall_lookup_1 (not ∘ P) l1); [by apply list_find_None|..].
-  Qed.
-  Lemma list_find_app_l l1 l2 i x:
-    list_find P l1 = Some (i, x) → list_find P (l1 ++ l2) = Some (i, x).
-  Proof. rewrite list_find_app_Some. auto. Qed.
-  Lemma list_find_app_r l1 l2:
-    list_find P l1 = None →
-    list_find P (l1 ++ l2) = prod_map (λ x, x + length l1) id <$> list_find P l2.
-  Proof.
-    intros. apply option_eq; intros [j y]. rewrite list_find_app_Some. split.
-    - intros [?|(?&?&->)]; naive_solver auto with f_equal lia.
-    - intros ([??]&->&?)%fmap_Some; naive_solver auto with f_equal lia.
-  Qed.
-
-  Lemma list_find_insert_Some l i j x y :
-    list_find P (<[i:=x]> l) = Some (j,y) ↔
-      (j < i ∧ list_find P l = Some (j,y)) ∨
-      (i = j ∧ x = y ∧ j < length l ∧ P x ∧ ∀ k z, l !! k = Some z → k < i → ¬P z) ∨
-      (i < j ∧ ¬P x ∧ list_find P l = Some (j,y) ∧ ∀ z, l !! i = Some z → ¬P z) ∨
-      (∃ z, i < j ∧ ¬P x ∧ P y ∧ P z ∧ l !! i = Some z ∧ l !! j = Some y ∧
-            ∀ k z, l !! k = Some z → k ≠ i → k < j → ¬P z).
-   Proof.
-     split.
-     - intros ([(->&->&?)|[??]]%list_lookup_insert_Some&?&Hleast)%list_find_Some.
-       { right; left. split_and!; [done..|]. intros k z ??.
-         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
-       assert (j < i ∨ i < j) as [?|?] by lia.
-       { left. rewrite list_find_Some. split_and!; [by auto..|]. intros k z ??.
-         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
-       right; right. assert (j < length l) by eauto using lookup_lt_Some.
-       destruct (lookup_lt_is_Some_2 l i) as [z ?]; [lia|].
-       destruct (decide (P z)).
-       { right. exists z. split_and!; [done| |done..|].
-         + apply (Hleast i); [|done]. by rewrite list_lookup_insert by lia.
-         + intros k z' ???.
-           apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
-       left. split_and!; [done|..|naive_solver].
-       + apply (Hleast i); [|done]. by rewrite list_lookup_insert by lia.
-       + apply list_find_Some. split_and!; [by auto..|]. intros k z' ??.
-         destruct (decide (k = i)) as [->|]; [naive_solver|].
-         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia.
-     - intros [[? Hl]|[(->&->&?&?&Hleast)|[(?&?&Hl&Hnot)|(z&?&?&?&?&?&?&?Hleast)]]];
-         apply list_find_Some.
-       + apply list_find_Some in Hl as (?&?&Hleast).
-         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
-         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
-       + rewrite list_lookup_insert by done. split_and!; [by auto..|].
-         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
-       + apply list_find_Some in Hl as (?&?&Hleast).
-         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
-         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
-       + rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
-         intros k z' [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
-  Qed.
-
-  Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l :
-    (∀ x, P x ↔ Q x) →
-    list_find P l = list_find Q l.
-  Proof.
-    intros HPQ. induction l as [|x l IH]; simpl; [done|].
-    by rewrite (decide_ext (P x) (Q x)), IH by done.
-  Qed.
-End find.
-
 Lemma TCForall_Forall {A} (P : A → Prop) xs : TCForall P xs ↔ Forall P xs.
 Proof. split; induction 1; constructor; auto. Qed.